proposition: Lemma Rminus_eq_compat_l : forall r r1 r2 : R, r1 = r2 <-> r - r1 = r - r2.
proof: Proof. split ; intros. apply Rplus_eq_compat_l. rewrite H. reflexivity. replace r1 with (r-(r-r1)) by ring. replace r2 with (r-(r-r2)) by ring. apply Rplus_eq_compat_l. rewrite H. reflexivity. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)