proposition: Lemma leq_addLR m n p : n <= p -> (m + n <= p) = (m <= p - n).
proof: Proof. by move => H; rewrite -!subn_eq0 subnBA. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2