proposition: Lemma length_leP_le_2 : forall O E E' A B C D AB CD, Length O E E' A B AB -> Length O E E' C D CD -> Le A B C D -> LeP O E E' AB CD.
proof: Proof. intros. assert(HH1:= length_Ar2 O E E' A B AB H). assert(HH2:= length_Ar2 O E E' C D CD H0). spliter. unfold Length in *. spliter. apply bet_leP; try assumption. induction(eq_dec_points O CD). subst CD. apply cong_symmetry in H4. apply cong_identity in H4. subst D. unfold Le in H1. ex_and H1 X. apply between_identity in H1. subst X. apply cong_identity in H4. subst B. apply cong_identity in H7. subst AB. Between. assert(Le O AB O CD). apply(l5_6 A B C D O AB O CD); Cong. unfold Le in H8. ex_and H9 M. induction HH1; induction HH2. spliter. unfold Le in H1. ex_and H1 P. unfold LeP in *. induction H6; induction H3. unfold LtP in *. ex_and H6 X. ex_and H3 Y. apply diff_sum in H6. apply diff_sum in H3. apply sum_cong in H6; auto. apply sum_cong in H3; auto. unfold Parallelogram_flat in *. spliter. apply cong_symmetry in H19. apply cong_identity in H19. subst Y. apply cong_symmetry in H23. apply cong_identity in H23. subst X. clean_trivial_hyps. assert(AB = M \/ Midpoint O AB M). apply(l7_20 O AB M); Cong. unfold Ps in *. assert(Out O AB CD). apply (l6_7 O AB E CD); auto. apply l6_6. assumption. apply out_col in H3. apply bet_col in H9. apply col_permutation_2. apply (col_transitivity_1 _ CD); Col. induction H3. subst M. assumption. unfold Midpoint in H3. spliter. assert(Out O AB CD). unfold Ps in *. apply (l6_7 O AB E CD); auto. apply l6_6. assumption. assert(Bet AB O CD). eapply (outer_transitivity_between _ _ M); Between. intro. subst M. apply cong_identity in H6. subst AB. tauto. unfold Out in H18. spliter. induction H22. assert(AB = O). apply(between_equality _ _ CD); Between. subst AB. Between. assert(Bet CD O CD). apply (between_exchange3 AB); Between. assert(O = CD). apply between_equality in H23. contradiction. Between. tauto. right. intro. subst Y. unfold Ps in H17. unfold Out in H17. tauto. right. intro. subst X. unfold Ps in H16. unfold Out in H16. tauto. subst CD. tauto. subst AB. Between. subst CD. tauto. subst CD. tauto. subst AB. Between. subst CD. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order