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