proposition: Lemma Rdiv_minus : forall a b c d : R, b <> 0 -> d <> 0 -> a / b - c / d = (a * d - c * b) / (b * d).
proof: Proof. intros. field. split. apply H0. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)