proposition: Lemma distance_vecteur : forall A B : PO, A <> B -> vec A B = mult_PP (distance A B) (representant_unitaire (vec A B)).
proof: Proof. unfold distance in |- *; intros. elim existence_representant_unitaire with (A := A) (B := B); [ intros C H0; try clear existence_unitaire; try exact H0 | auto ]. rewrite <- H0; auto. rewrite (caract_representant_unitaire (A:=A) (B:=B) (C:=C)); auto. unfold distance in |- *. cut (sqrt (scalaire (vec A B) (vec A B)) <> 0); intros. Fieldvec (sqrt (scalaire (vec A B) (vec A B))). auto with *. Qed.