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