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