proposition: Lemma orthogonal_alignement : forall A B C D : PO, A <> B -> alignes A B C -> orthogonal (vec A B) (vec C D) -> orthogonal (vec C D) (vec C B).
proof: Proof. intros. halignes H0 x. apply ortho_sym. replace (vec C B) with (add_PP (vec A B) (mult_PP (-1) (vec A C))). rewrite H2. replace (add_PP (vec A B) (mult_PP (-1) (mult_PP x (vec A B)))) with (mult_PP (1 + - x) (vec A B)). Simplortho. Ringvec. Ringvec. Qed.