proposition: Lemma alignement_triangle : forall A B C D E : PO, A <> D :>PO -> A <> E :>PO -> triangle A B C -> alignes A B D -> alignes A C E -> triangle A D E.
proof: Proof. intros. deroule_triangle A B C. apply angle_non_alignes; auto with geo. rewrite <- (alignement_et_angles (A:=A) (B:=B) (C:=D) (D:=A) (E:=C) (F:=E)); auto with geo. Qed.