proposition: Lemma Rdist_sym : forall x y:R, Rdist x y = Rdist y x.
proof: Proof. unfold Rdist; intros; split_Rabs; try ring. - generalize (Ropp_gt_lt_0_contravar (y - x) Hlt0); intro; rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 Hlt); intro; unfold Rgt in H; exfalso; auto. - generalize (minus_Rge y x Hge0); intro; generalize (minus_Rge x y Hge); intro; generalize (Rge_antisym x y H0 H); intro; rewrite H1; ring. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac