proposition: Lemma l7_25 : forall A B C, Cong C A C B -> exists X, Midpoint X A B.
proof: Proof. intros. induction(col_dec A B C). assert(A = B \/ Midpoint C A B). apply l7_20. unfold Col in *. intuition. assumption. induction H1. subst B. exists A. apply l7_3_2. exists C. assumption. assert (exists P, Bet C A P /\ A<>P). apply point_construction_different. ex_and H1 P. prolong C B Q A P. assert (exists R, Bet A R Q /\ Bet B R P). eapply inner_pasch. apply between_symmetry. apply H1. apply between_symmetry. assumption. ex_and H5 R. assert (exists X, Bet A X B /\ Bet R X C). eapply inner_pasch. apply H1. assumption. ex_and H7 X. exists X. unfold Midpoint. split. assumption. apply cong_left_commutativity. cut(Cong R A R B). intros. induction(eq_dec_points R C). subst R. assert (C = X). apply between_identity. assumption. subst X. assumption. eapply l4_17. apply H10. unfold Col. right; left. apply between_symmetry. assumption. assumption. assumption. assert (OFSC C A P B C B Q A). unfold OFSC. repeat split. assumption. assumption. assumption. apply cong_symmetry. assumption. apply cong_symmetry. assumption. apply cong_pseudo_reflexivity. assert (Cong P B Q A). eapply five_segment_with_def. eapply H9. unfold Col in H0. intuition. apply H0. subst A. apply between_trivial. assert (exists R', Bet A R' Q /\ Cong_3 B R P A R' Q). eapply l4_5. assumption. apply cong_commutativity. assumption. ex_and H11 R'. assert (IFSC B R P A A R' Q B). unfold IFSC. repeat split. assumption. assumption. apply cong_commutativity. assumption. unfold Cong_3 in H12. spliter. assumption. apply cong_pseudo_reflexivity. apply cong_commutativity. apply cong_symmetry. assumption. assert (IFSC B R P Q A R' Q P). unfold IFSC. repeat split;try assumption. apply cong_commutativity. assumption. unfold Cong_3 in H12. spliter. assumption. apply cong_pseudo_reflexivity. assert (Cong R A R' B). eapply l4_2. apply H13. assert (Cong R Q R' P). eapply l4_2. apply H14. assert (Cong_3 A R Q B R' P). unfold Cong_3. repeat split. apply cong_commutativity. assumption. apply cong_commutativity. apply cong_symmetry. assumption. assumption. assert (Col B R' P). apply (l4_13 A R Q); Col. cut(R=R'). intro. subst R'. assumption. assert (B <> P). unfold IFSC, OFSC, Cong_3 in *. spliter. intro. subst P. apply between_identity in H14. subst R. apply cong_reverse_identity in H12. subst R'. apply cong_reverse_identity in H32. subst Q. apply between_identity in H5. apply H2. assumption. assert (A <> Q). unfold IFSC, OFSC, Cong_3 in *. spliter. intro. subst Q. apply cong_reverse_identity in H20. subst P. apply H19. reflexivity. assert(B <> Q). intro. subst Q. apply cong_symmetry in H4. apply cong_identity in H4. subst P. apply H2. reflexivity. assert (B <> R). intro. unfold Cong_3, IFSC, OFSC in *. spliter. subst R. clean_duplicated_hyps. assert (Col B A C). apply col_transitivity_1 with X; Col. intro. apply cong_symmetry in H12. apply cong_identity in H12. subst R'. subst X. clean_duplicated_hyps. assert (Bet B A C \/ Bet B C A). apply l5_2 with Q; Between. apply H0. unfold Col. induction H9. right;right. apply between_symmetry. assumption. right; left. assumption. apply H0. apply col_permutation_4. assumption. eapply (l6_21 A Q B P R R' ). intro. unfold Col in H23. induction H23. assert(Bet A B C). eapply outer_transitivity_between2. apply H23. apply between_symmetry. assumption. intro. apply H21. rewrite H24. reflexivity. apply H0. unfold Col. left. assumption. induction H23. assert(Bet B A C \/ Bet B C A). apply (l5_2 Q); Between. apply H0. unfold Col. induction H24. right;right. apply between_symmetry. assumption. right; left. assumption. assert(Bet A B C). eapply between_exchange3. apply between_symmetry. apply H23. apply between_symmetry. assumption. apply H0. unfold Col. left. assumption. assumption. unfold Col. right; left. apply between_symmetry. assumption. unfold Col. right; left. apply between_symmetry. assumption. unfold Col. right; left. apply between_symmetry. assumption. unfold Col. unfold Col in H18. induction H18. right; left. apply between_symmetry. assumption. induction H18. left. apply between_symmetry. assumption. right;right. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR