proposition: Lemma Rdist_tri : forall x y z:R, Rdist x y <= Rdist x z + Rdist z y.
proof: Proof. intros; unfold Rdist; replace (x - y) with (x - z + (z - y)); [ apply (Rabs_triang (x - z) (z - y)) | ring ]. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac