proposition: Lemma leR_add2r {p m n} : m + p <= n + p <-> m <= n.
proof: Proof. by split; [exact: Rplus_le_reg_r | exact: Rplus_le_compat_r]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)