Open vblot opened 5 years ago
https://github.com/esum/internship2019/blob/085f9866cbbc9efa76223009585bc8bbec3d6ee1/src/seq2.v#L41 ce lemme n'est pas vraiment nécessaire. Son utilisation ici : https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L719 peut être remplacée par :
rewrite (@eq_map _ _ _ (fun p => (p, logn p n))); last first. move=> p ; by rewrite H. congr map.
https://github.com/esum/internship2019/blob/085f9866cbbc9efa76223009585bc8bbec3d6ee1/src/seq2.v#L41 ce lemme n'est pas vraiment nécessaire. Son utilisation ici : https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L719 peut être remplacée par :