Open vblot opened 5 years ago
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/seq2.v#L51 ce lemme n'est pas vraiment nécessaire. Son utilisation ici : https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L741 peut être remplacée par :
have ->: primes m = primes n; last first. apply eq_in_map. move=> p p_in ; rewrite H //. rewrite mem_primes in p_in. move/and3P in p_in. by destruct p_in.
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/seq2.v#L51 ce lemme n'est pas vraiment nécessaire. Son utilisation ici : https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L741 peut être remplacée par :