proposition: Lemma alignes_angle : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> double_AV (cons_AV (vec A B) (vec A C)) = image_angle 0 -> alignes A B C.
proof: Proof. intros. cut (paralleles (droite A B) (droite A C)); intros. elim (paralleles_vecteur (A:=A) (B:=B) (C:=A) (D:=C)); auto; intros. lapply (colineaire_alignes (k:=x) (A:=A) (B:=C) (C:=B)); auto with geo. apply droites_paralleles_angle; auto. Qed.