proposition: Lemma ltR_subRL m n p : (n < p - m) <-> (m + n < p).
proof: Proof. split => H. - by move/(@ltR_add2l m) : H; rewrite subRKC. - by apply (@ltR_add2l m); rewrite subRKC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)