proposition: Lemma egalite_scalaire_alignes : forall A B C D : PO, A <> B -> alignes A B C -> alignes A B D -> scalaire (vec A B) (vec A C) = scalaire (vec A B) (vec A D) -> C = D.
proof: Proof. intros. halignes H0 x. halignes H1 x0. assert (x = x0). apply Rmult_eq_reg_l with (scalaire (vec A B) (vec A B)); auto with geo real. replace (scalaire (vec A B) (vec A B) * x) with (scalaire (vec A B) (vec A C)). rewrite H2; rewrite H4; Simplscal. rewrite H3; Simplscal. apply egalite_vecteur_point with A. rewrite H3; rewrite H5; rewrite H4; auto. Qed.