proposition: Lemma distance_1_representant : forall A B : PO, distance A B = 1 -> vec A B = representant_unitaire (vec A B).
proof: Proof. intros. apply def_representant_unitaire; auto with geo. rewrite carre_scalaire_distance; rewrite H; ring. Qed.