proposition: Lemma carre_scalaire_egalite_distance : forall A B C D : PO, scalaire (vec A B) (vec A B) = scalaire (vec C D) (vec C D) -> distance A B = distance C D.
proof: Proof. intros. apply carre_egalite_distance. repeat rewrite <- carre_scalaire_distance; auto with geo. Qed.