proposition: Lemma distance_nulle : forall A B : PO, scalaire (vec A B) (vec A B) = 0 :>R -> A = B.
proof: Proof. intros. cut (vec A B = zero); intros. unfold vec in H0. apply conversion_PP with (a := 1) (b := 1); auto with *. RingPP2 H0; RingPP. apply scalaire_non_degenere; auto. Qed.