You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Lemma ltn_leq_trans : forall x y z, ltn x y -> leq y z -> ltn x z.
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.
The text was updated successfully, but these errors were encountered:
internship2019/src/arith.v
Line 35 in 17e55db
Ce lemme est en fait une instance de leq_trans car
m<n
est codé parm.+1<=n
. Du coup tu peux remplacer partout ltn_leq_trans par leq_trans et supprimer ce lemme.The text was updated successfully, but these errors were encountered: