proposition: Lemma Rdist_eq : forall x:R, Rdist x x = 0.
proof: Proof. unfold Rdist; intros; split_Rabs; intros; ring. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac