proposition: Lemma dist_non_nulle : forall A B : PO, distance A B <> 0 -> A <> B.
proof: Proof. unfold distance in |- *; red in |- *; intros. apply H. rewrite H0. replace (scalaire (vec B B) (vec B B)) with 0. rewrite sqrt_0; ring. replace (vec B B) with (mult_PP 0 (vec A B)). Simplscal. Ringvec. Qed.