proposition: Lemma alignes_unitaire : forall A B C : PO, alignes A B C -> scalaire (vec A B) (vec A B) = 1 -> vec A C = mult_PP (scalaire (vec A B) (vec A C)) (vec A B).
proof: Proof. intros. assert (A <> B); auto with geo. halignes H x. pattern (vec A C) at 2 in |- *. rewrite H2. Simplscal. rewrite H0; rewrite H2. RingPP. Qed.