proposition: Lemma angles_droites_paralleles : forall A B C D E F G I : PO, A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> G <> I :>PO -> paralleles (droite E F) (droite A B) -> paralleles (droite G I) (droite C D) -> cons_AD (droite A B) (droite C D) = cons_AD (droite E F) (droite G I) :>AD.
proof: Proof. intros A B C D E F G I H H0 H1 H2 H3 H4; try assumption. elim (paralleles_vecteur (A:=E) (B:=F) (C:=A) (D:=B)); auto. intros x H5; try assumption. elim (paralleles_vecteur (A:=G) (B:=I) (C:=C) (D:=D)); auto. intros x0 H6; try assumption. apply angles_droites_colinearite with (k1 := x) (k2 := x0); auto. Qed.