proposition: Lemma Rdist_refl : forall x y:R, Rdist x y = 0 <-> x = y.
proof: Proof. unfold Rdist; intros; split_Rabs; split; intros. - rewrite (Ropp_minus_distr x y) in H; symmetry; apply (Rminus_diag_uniq y x H). - rewrite (Ropp_minus_distr x y); generalize (eq_sym H); intro; apply (Rminus_diag_eq y x H0). - apply (Rminus_diag_uniq x y H). - apply (Rminus_diag_eq x y H). Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac