search

esum / internship2019

0 stars 0 forks source link

factorisation de preuves #14

Open vblot opened 5 years ago

vblot commented 5 years ago

https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L377-L392 ce morceau de preuve est répété deux fois d'affilée. Il serait mieux de prouver par exemple le lemme :

forall p m, coprime p m -> all (coprime p) (primes m).
vblot commented 5 years ago

idem ici : https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L416-L441

vblot commented 5 years ago

J'en ai encore repéré plusieurs à d'autres endroits, il faudrait reprendre tes preuves et essayer de factoriser partout où il y a du copier-coller.