proposition: Lemma l8_18_existence : forall A B C, ~ Col A B C -> exists X, Col A B X /\ Perp A B C X.
proof: Proof. intros. prolong B A Y A C. assert (exists P, Midpoint P C Y) by (apply l7_25 with A;Cong). ex_and H2 P. assert (Per A P Y) by (unfold Per;exists C;auto using l7_2). prolong A Y Z Y P. prolong P Y Q Y A. prolong Q Z Q' Q Z. assert (Midpoint Z Q Q') by (unfold Midpoint;split;Cong). prolong Q' Y C' Y C. assert (exists X, Midpoint X C C') by (apply l7_25 with Y;Cong). ex_and H13 X. assert (OFSC A Y Z Q Q Y P A) by (unfold OFSC;repeat split;Between;Cong). show_distinct A Y. intuition. assert (Cong Z Q P A) by (eauto using five_segment_with_def). assert (Cong_3 A P Y Q Z Y) by (unfold Cong_3;repeat split;Cong). assert (Per Q Z Y) by (eauto using l8_10). assert (Per Y Z Q) by eauto using l8_2. show_distinct P Y. apply H; Col. unfold Per in H19. ex_and H19 Q''. assert (Q' = Q''). eapply symmetric_point_uniqueness. apply H10. assumption. subst Q''. assert (hy:Bet Z Y X). apply (l7_22 Q C Q' C' Y Z X);Cong. assert (T:=outer_transitivity_between2 C P Y Q). assert_bets. apply between_symmetry. apply T;Between. show_distinct Q Y. intuition. assert (Per Y X C) by (unfold Per;exists C';split;Cong). assert_diffs. assert (Col P Y Q). unfold Col. left. assumption. assert(Col P Y C). unfold Midpoint in H3. spliter. unfold Col. right; right. assumption. assert (Col P Q C) by ColR. assert (Col Y Q C) by ColR. assert (Col A Y B) by Col. assert (Col A Y Z) by Col. assert (Col A B Z) by ColR. assert (Col Y B Z) by ColR. assert (Col Q Y P) by Col. assert(Q <> C). intro. subst Q. unfold Midpoint in *. spliter. apply H. assert (Bet B Y Z) by (apply outer_transitivity_between2 with A;auto). apply between_symmetry in H3. assert (Y = P). eapply between_equality. apply H3. assumption. treat_equalities. intuition. assert (Col Y B Z) by ColR. show_distinct Y Q'. intuition. assert (Col Y Q' C') by Col. assert (Q <> Q'). intro. unfold OFSC, Cong_3 in *. spliter. treat_equalities. apply H. ColR. assert (C <> C'). intro. subst C'. apply l7_3 in H14. subst X. assert (Col Z Q Q') by ColR. assert (Y <> Z). intro. subst Z. unfold OFSC, Cong_3, Midpoint in *. spliter. treat_equalities. intuition. apply H. ColR. assert(OFSC Q Y C Z Q' Y C' Z). unfold OFSC. repeat split;Between;Cong. unfold OFSC, Midpoint in *. spliter. eapply outer_transitivity_between with P;Between;Cong. assert (Cong C Z C' Z) by (eauto using five_segment_with_def). assert (Col Z Y X) by Col. show_distinct Y Z. intuition. assert(C <> X). intro. subst X. unfold OFSC,Cong_3,Midpoint in *. spliter. treat_equalities. intuition. assert(X <> Y). intro. subst X. unfold OFSC,Cong_3,Midpoint in *. spliter. clean_duplicated_hyps. clean_trivial_hyps. show_distinct C' Y. intuition. assert (Col Y C' P ). eapply col_transitivity_1 with C. intuition. unfold Col. right;right. apply between_symmetry. assumption. apply col_permutation_1. assumption. show_distinct P Q. intuition. assert (Col Y P Q') by ColR. assert (Col Y Q Q') by ColR. assert (Col Q Y Z) by ColR. assert (Col Y Z C) by ColR. apply H. ColR. assert (Perp_at X Y Z C X). eapply l8_13_2;Col. exists Y. exists C. repeat split;Col. assert (Col A B X) by ColR. exists X. split. assumption. unfold Perp. exists X. unfold Perp_at. repeat split;Col. intros. unfold Perp_at in H52. spliter. apply H57;ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR