proposition: Lemma distincts_dist_non_nulle : forall A B : PO, A <> B -> distance A B <> 0.
proof: Proof. unfold distance in |- *; intros; red in |- *; intros. apply H. apply distance_nulle. rewrite <- (def_sqrt (scalaire (vec A B) (vec A B))); auto with geo. rewrite H0; ring. Qed.