proposition: Lemma Rdist_mult_l : forall a b c, Rdist (a * b) (a * c) = Rabs a * Rdist b c.
proof: Proof. unfold Rdist. intros a b c; rewrite <- Rmult_minus_distr_l, Rabs_mult; reflexivity. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac