proposition: Lemma l12_23 : forall A B C, ~Col A B C -> exists B', exists C', TS A C B B' /\ TS A B C C' /\ Bet B' A C' /\ CongA A B C B A C' /\ CongA A C B C A B'.
proof: Proof. intros. assert(exists B0, Midpoint B0 A B) by (apply midpoint_existence). assert(exists C0, Midpoint C0 A C) by (apply midpoint_existence). ex_and H0 B0. ex_and H1 C0. prolong B C0 B' B C0. prolong C B0 C' C B0. exists B'. exists C'. assert(TS A C B B'). apply mid_two_sides with C0; Col. split. assumption. Cong. assert(TS A B C C'). eapply mid_two_sides with B0; Col. split. assumption. Cong. split. assumption. split. assumption. assert(Par A B' C B). eapply l12_17. intro. treat_equalities. assert(C0 = B0). apply (l7_17 A B). split. apply between_symmetry. assumption. Cong. assumption. treat_equalities. Col. apply H0. split. apply between_symmetry. assumption. Cong. assert(Par A C' B C). eapply l12_17. intro. treat_equalities. assert(C0 = B0). eapply l7_17. apply H0. split. apply between_symmetry. assumption. Cong. treat_equalities. Col. apply H2. split. apply between_symmetry. assumption. Cong. assert(Par A B' A C'). eapply par_trans. apply H8. apply par_symmetry. apply par_right_comm. assumption. apply par_id in H10. assert(OS A C B0 C'). eapply out_one_side_1. intro. apply H. assert_diffs. eapply (col_transitivity_1 _ B0); Col. apply col_trivial_2. apply bet_out. intro. treat_equalities. assert_diffs; auto. assumption. assert(OS A C B0 B). eapply out_one_side_1. intro. apply H. eapply (col_transitivity_1 _ B0); Col. intro. treat_equalities. Col. apply col_trivial_3. assert_diffs; apply bet_out; Between. assert(OS A C B C'). apply one_side_transitivity with B0. apply one_side_symmetry. assumption. assumption. assert(TS A C B' C'). apply l9_2. eapply l9_8_2. apply H6. assumption. split. apply col_two_sides_bet with C; assumption. split. apply l9_2 in H7. assert(HH:= l12_21_a A C' B C H7 H9); CongA. apply par_symmetry in H8. apply invert_two_sides in H6. assert(HH:= l12_21_a C B A B' H6 H8); CongA. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID