proposition: Lemma non_alignes_angle : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> ~ alignes A B C -> double_AV (cons_AV (vec A B) (vec A C)) <> image_angle 0 :>AV.
proof: Proof. red in |- *; intros. apply H1. apply alignes_angle; auto with geo. Qed.