Open vblot opened 5 years ago
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L35 Ce lemme est en fait une instance de leq_trans car m<n est codé par m.+1<=n. Du coup tu peux remplacer partout ltn_leq_trans par leq_trans et supprimer ce lemme.
m<n
m.+1<=n
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L35 Ce lemme est en fait une instance de leq_trans car
m<nest codé parm.+1<=n. Du coup tu peux remplacer partout ltn_leq_trans par leq_trans et supprimer ce lemme.