proposition: Lemma 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 A B C D H H0 H10 H1; try assumption. halignes H0 k. halignes H10 k'. rewrite H2 in H1. rewrite H3 in H1. repeat rewrite scalaire_mult_d in H1. elim (classic (k = k')); intros. rewrite H4 in H2. cut (vec A C = vec A D); intros. apply egalite_vecteur_point with A; auto. rewrite H2; rewrite H3; auto. absurd ((k + - k') * scalaire (vec A B) (vec A B) = 0); auto. apply integre_not; auto with geo. contrapose H4. RReplace k (k + - k' + k'). rewrite H5; ring. RReplace ((k + - k') * scalaire (vec A B) (vec A B)) (k * scalaire (vec A B) (vec A B) + - k' * scalaire (vec A B) (vec A B)). rewrite H1; ring. Qed.