proposition: Lemma l7_22_aux : forall A1 A2 B1 B2 C M1 M2, Bet A1 C A2 -> Bet B1 C B2 -> Cong C A1 C B1 -> Cong C A2 C B2 -> Midpoint M1 A1 B1 -> Midpoint M2 A2 B2 -> Le C A1 C A2 -> Bet M1 C M2.
proof: Proof. intros. induction (eq_dec_points A2 C). subst C. apply le_zero in H5. subst A2. apply cong_reverse_identity in H1. subst B1. apply cong_reverse_identity in H2. subst B2. apply l7_3 in H4. subst A1. apply between_trivial. assert (exists A, Midpoint C A2 A). apply symmetric_point_construction. induction H7. assert (exists B, Midpoint C B2 B). apply symmetric_point_construction. induction H8. assert (exists M, Midpoint C M2 M). apply symmetric_point_construction. induction H9. assert(Midpoint x1 x x0). unfold Midpoint. split. eapply l7_15. apply H7. apply H9. apply H8. unfold Midpoint in H4. spliter. assumption. eapply l7_16. apply H7. apply H9. apply H9. apply H8. unfold Midpoint in H4. spliter. assumption. assert (Le C A1 C x). eapply l5_6. repeat split. apply H5. apply cong_reflexivity. unfold Midpoint in H7. spliter. apply cong_left_commutativity. assumption. assert (Bet C A1 x). induction (eq_dec_points A1 C). subst A1. apply between_trivial2. apply l6_13_1; [|assumption]. unfold Out. repeat split. assumption. intro. subst x. apply le_zero in H11. apply H12. subst A1. reflexivity. eapply l5_2. apply H6. apply between_symmetry. assumption; intro. unfold Midpoint in H7. spliter. assumption. assert (Le C B1 C x0). eapply l5_6. apply H11. assumption. unfold Midpoint in *. spliter. eapply cong_transitivity. apply cong_symmetry. apply H16. apply cong_transitivity with B2 C. apply cong_commutativity. assumption. assumption. assert (Bet C B1 x0). induction (eq_dec_points B1 C). subst B1. apply cong_symmetry in H1. apply cong_reverse_identity in H1. subst A1. apply between_trivial2. induction (eq_dec_points x0 C). subst x0. apply le_zero in H13. subst B1. apply between_trivial. induction (eq_dec_points B2 C). subst B2. apply cong_symmetry in H2. eapply cong_reverse_identity in H2. subst A2. apply le_zero in H5. subst A1. apply cong_reverse_identity in H1. subst B1. apply False_ind. apply H14. reflexivity. eapply l6_13_1. unfold Out. repeat split. assumption. assumption. apply l5_2 with B2; Between. unfold Midpoint in H8. spliter. assumption. assumption. assert (exists Q, Bet x1 Q C /\ Bet A1 Q B1). eapply l3_17. apply between_symmetry. apply H12. apply between_symmetry. apply H14. unfold Midpoint in H10. spliter. assumption. ex_and H15 Q. assert (IFSC x A1 C x1 x0 B1 C x1). unfold IFSC. unfold Midpoint in *. spliter. repeat split. apply between_symmetry. assumption. apply between_symmetry. assumption. eapply cong_transitivity. apply cong_commutativity. apply cong_symmetry. apply H20. eapply cong_transitivity. apply H2. apply cong_commutativity. assumption. apply cong_commutativity. assumption. apply cong_right_commutativity. assumption. apply cong_reflexivity. assert (Cong A1 x1 B1 x1). eapply l4_2. apply H17. assert (Cong Q A1 Q B1). induction(eq_dec_points C x1). subst x1. apply between_identity in H15. subst Q. apply cong_commutativity. assumption. eapply l4_17. apply H19. unfold Col. right; left. assumption. assumption. apply cong_commutativity. assumption. assert (Midpoint Q A1 B1). unfold Midpoint. split. assumption. apply cong_left_commutativity. assumption. assert (Q=M1). eapply l7_17. apply H20. assumption. subst Q. eapply between_exchange3. apply H15. unfold Midpoint in H9. spliter. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR