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