proposition: Lemma angle_non_alignes : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> double_AV (cons_AV (vec A B) (vec A C)) <> image_angle 0 :>AV -> ~ alignes A B C.
proof: Proof. intros. cut (~ paralleles (droite A C) (droite A B)); intros. red in |- *; intros; apply H2. apply paralleles_sym; auto. apply alignes_paralleles; auto. apply angle_non_paralleles; auto. Qed.