proposition: Lemma Rdist_plus : forall a b c d:R, Rdist (a + c) (b + d) <= Rdist a b + Rdist c d.
proof: Proof. intros; unfold Rdist; replace (a + c - (b + d)) with (a - b + (c - d)). - exact (Rabs_triang (a - b) (c - d)). - ring. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac