proposition: Lemma Rlt_minus_l : forall a b c,(a - c < b <-> a < b + c).
proof: Proof. split ; intros. replace a with ((a-c)+c) by ring. apply Rplus_lt_compat_r. apply H. replace b with ((b+c)-c) by ring. apply Rplus_lt_compat_r. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)