proposition: Lemma le_transitivity : forall A B C D E F, Le A B C D -> Le C D E F -> Le A B E F.
proof: Proof. unfold Le. intros. ex_and H y. ex_and H0 z. assert (exists P : Tpoint, Bet E P z /\ Cong_3 C y D E P z) by (eapply l4_5;assumption). ex_and H3 P. exists P. split. eBetween. unfold Cong_3 in H4; spliter; apply cong_transitivity with C y; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col