proposition: Lemma per_cong : forall A B P R X , A <> B -> A <> P -> Per B A P -> Per A B R -> Cong A P B R -> Col A B X -> Bet P X R -> Cong A R P B.
proof: Proof. intros. assert (Per P A B). apply l8_2. assumption. double B R Q. assert (B <> R). intro. subst R. apply cong_identity in H3. subst P. absurde. assert (Per A B Q). eapply per_col. apply H8. assumption. unfold Col. left. apply midpoint_bet. assumption. assert (Per P A X). eapply per_col. apply H. assumption. assumption. assert (B <> Q). intro. subst Q. apply l7_3 in H7. subst R. absurde. assert (Per R B X). eapply per_col. intro. apply H. apply sym_equal. apply H12. apply l8_2. assumption. apply col_permutation_4. assumption. assert (X <> A). intro. subst X. assert (~Col P A R). eapply per_not_colp. apply H. assumption. assumption. assumption. assumption. apply H13. unfold Col. left. assumption. double P A P'. prolong P' X R' X R. assert (exists M, Midpoint M R R'). eapply l7_25. apply cong_symmetry. apply H16. ex_elim H17 M. assert (Per X M R). unfold Per. exists R'. split. assumption. apply cong_symmetry. assumption. assert (Cong X P X P'). apply l8_2 in H10. unfold Per in H10. ex_and H10 P''. assert (P'=P''). eapply symmetric_point_uniqueness. apply H14. apply H10. subst P''. assumption. assert (X <> P'). intro. subst P'. apply cong_identity in H19. subst X. apply l7_3 in H14. subst P. absurde. assert (P <> P'). intro. subst P'. eapply l7_3 in H14. subst P. absurde. assert(~Col X P P'). intro. assert(Col X P A). eapply col3. apply H21. apply col_permutation_1. assumption. apply col_trivial_3. unfold Col. right;left. apply between_symmetry. apply midpoint_bet. assumption. apply col_permutation_1 in H23. assert (P = A \/ X = A). eapply l8_9. assumption. assumption. induction H24. subst P. absurde. apply H13. assumption. assert (Bet A X M). apply (l7_22 P R P' R'); trivial. apply cong_symmetry. assumption. assert (X <> R). intro. treat_equalities. apply l8_8 in H12. treat_equalities. unfold Midpoint in *. spliter. treat_equalities. intuition. assert (X <> R'). intro. subst R'. apply cong_symmetry in H16. apply cong_identity in H16. apply H24. assumption. assert (M <> X). intro. subst M. apply H22. eapply col_transitivity_1. apply H24. unfold Col. right; right. assumption. eapply col_transitivity_1. apply H25. unfold Col. right;right. apply midpoint_bet. assumption. unfold Col. right; right. assumption. assert (M = B). eapply (l8_18_uniqueness A X R). intro. assert (Col A B R). eapply col_transitivity_1. intro. apply H13. apply sym_equal. apply H28. apply col_permutation_5. assumption. assumption. eapply per_not_col. apply H; apply H12. apply H8. assumption. assumption. unfold Col. left. assumption; eapply col_transitivity_1. apply per_perp in H17. apply perp_comm. eapply perp_col. assumption. apply H17. unfold Col. right;right. assumption. auto. intro. subst M. apply (symmetric_point_uniqueness R R R R') in H18. subst R'. apply H22. eapply col_transitivity_1. apply H25. unfold Col. right;right. assumption. unfold Col. right; right. assumption. eapply l7_3_2. apply col_permutation_5. assumption. apply per_perp in H10. apply perp_comm. eapply perp_col. apply H13. apply perp_comm. eapply perp_col. intro. apply H13. apply sym_equal. apply H27. apply perp_right_comm. apply per_perp in H2. apply H2. assumption. assumption. assumption. apply col_trivial_2. auto. intro. apply H13. subst X. reflexivity. subst M. assert(OFSC P X R P' P' X R' P). unfold OFSC. repeat split. assumption. assumption. apply cong_commutativity. assumption. apply cong_symmetry. assumption. apply cong_pseudo_reflexivity. apply cong_symmetry. assumption. assert (Cong R P' R' P). eapply five_segment_with_def. apply H27. intro. subst X. apply H22. apply col_trivial_1. assert (IFSC P' A P R R' B R P). unfold IFSC. repeat split. apply between_symmetry. apply midpoint_bet. assumption. apply between_symmetry. apply midpoint_bet. assumption. eapply l2_11. apply between_symmetry. apply midpoint_bet. apply H14. apply between_symmetry. apply midpoint_bet. apply H18. eapply cong_transitivity. apply midpoint_cong. apply l7_2. apply H14. eapply cong_transitivity. apply H3. apply cong_commutativity. apply midpoint_cong. assumption. assumption. assumption. Cong. apply cong_pseudo_reflexivity. eapply cong_right_commutativity. eapply l4_2. eapply H29. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR