proposition: Lemma Rle_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_le_compat_r. apply H. replace a with ((a+c)-c) by ring. apply Rplus_le_compat_r. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)