proposition: Lemma leq_addLRI m n p : (m + n <= p) -> (m <= p - n).
proof: Proof. move=> Hmnp. - have Hnp : n <= p by exact: leq_trans (leq_addl _ _) Hmnp. - move: Hmnp; rewrite -!subn_eq0 subnBA //. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2