proposition: Lemma alignes_non_orthogonal : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> alignes A B C -> ~ orthogonal (vec A B) (vec A C).
proof: Proof. intros. halignes H1 x. cut (x <> 0); intros. 2: apply distinct_col_nonzero with (2 := H2); auto. apply non_orthogonal_def. rewrite H2. Simplscal. apply integre_not; auto with geo. Qed.