proposition: Lemma Rdiv_minus_distr : forall a b c, (a - b) / c = a / c - b / c.
proof: Proof. unfold Rminus; intros r1 r2 r. now rewrite Ropp_div_distr_l; apply Rdiv_plus_distr. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField