proposition: Lemma distance_refl : forall A B : PO, distance A B = 0 <-> A = B.
proof: Proof. unfold distance in |- *; intros; red in |- *. split; [ idtac | try assumption ]. intros H; try assumption. apply distance_nulle. RReplace 0 (0 * 0). rewrite <- H; auto. symmetry in |- *. apply def_sqrt; auto with geo real. intros. rewrite <- H; auto. VReplace (vec A A) (mult_PP (-0) (vec A B)). Simplscal. replace (-0 * -0 * scalaire (vec A B) (vec A B)) with 0; try ring. try exact sqrt_0. Qed.