proposition: Lemma ltn_leq_pred m n : m < n -> m <= n.-1.
proof: Proof. by move=> H; rewrite -ltnS (ltn_predK H). Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2