proposition: Lemma l9_3 : forall P Q A C M R B, TS P Q A C -> Col M P Q -> Midpoint M A C -> Col R P Q -> Out R A B -> TS P Q B C.
proof: Proof. Proof with Col. intros. unfold TS in *. assert (~ Col A P Q). spliter. assumption. spliter. clear H. assert (P <> Q). intro. subst Q. Col. ex_and H6 T. show_distinct A C. intuition. assert (T = M). assert_bets. assert_cols. eapply l6_21 with P Q A C... subst T. repeat split... induction(eq_dec_points C M). subst M. intuition. intro. clear H0. assert (B <> R). intro. subst B. unfold Out in H3. spliter. absurde. assert (Col P R B) by ColR. assert (Col P R A). induction (eq_dec_points P B). subst B. assert_cols... apply col_permutation_2. eapply col_transitivity_2. apply H0. assert_cols... Col. induction (eq_dec_points P R). subst R. apply H4. apply col_permutation_2. eapply (col_transitivity_1 _ B). assert_diffs;intuition. apply col_permutation_4. assumption. assert_cols... assert (Col P B A ). eapply col_transitivity_1. apply H13. assumption. assumption. induction (eq_dec_points P B). subst B. apply H4. apply col_permutation_2. eapply (col_transitivity_1 _ R). apply H0. apply col_permutation_4. assumption. unfold Out in H3. spliter. unfold Col. induction H16. right; left. assumption. right;right. Between. apply H4. apply col_permutation_2. eapply col_transitivity_1. apply H15. Col. assumption. induction H3. spliter. induction H10. double B M B'. double R M R'. assert (Bet B' C R'). eapply l7_15. apply H11. apply H1. apply H12. Between. assert (exists X, Bet M X R' /\ Bet C X B). eapply inner_pasch. apply midpoint_bet. apply H11. apply between_symmetry. assumption. ex_and H14 X. exists X. split. assert (Col P M R ). eapply col_transitivity_1. apply H. Col. Col. assert (Col Q M R). eapply (col_transitivity_1 _ P). auto. Col. Col. induction (eq_dec_points M X). subst X. assumption. show_distinct M R'. intuition. assert (M <> R). intro. subst R. eapply (symmetric_point_uniqueness) in H12. apply H19. apply H12. apply l7_3_2. apply col_permutation_2. ColR. Between. assert (exists X, Bet B X C /\ Bet M X R). eapply inner_pasch. apply H10. Between. ex_and H11 X. exists X. induction (eq_dec_points M R). subst R. apply between_identity in H12. subst X. split; assumption. induction (eq_dec_points R X). subst X. split; assumption. split. induction (eq_dec_points X M). subst X. assumption. assert (Col P M R ). eapply col_transitivity_1. apply H. Col. Col. assert (Col X P Q). apply col_permutation_2. ColR. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar