proposition: Lemma ltR_subl_addl x y z : (x - y < z) <-> (x < y + z).
proof: Proof. split => [/(@ltR_add2r y)|/(@ltR_add2r (- y))]; first by rewrite subRK addRC. by rewrite addR_opp (addRC y) addR_opp addRK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)