proposition: Lemma angle_construction_2 : forall A B C A' B' P, A <> B -> A <> C -> B <> C -> A' <> B' -> ~ Col A' B' P -> exists C', CongA A B C A' B' C' /\ (OS A' B' C' P \/ Col A' B' C').
proof: Proof. intros. spliter. induction (col_dec A B C). induction (out_dec B A C). exists A'. split. assert(CongA A B A A B C). apply out2__conga. apply out_trivial. auto. apply l6_6. assumption. assert (CongA A B A A' B' A'). apply conga_trivial_1. auto. auto. apply conga_sym. eapply conga_trans. apply conga_sym. apply H7. assumption. right. apply col_trivial_3. apply not_out_bet in H5. prolong A' B' C' A' B'. exists C'. split. eapply conga_line; try assumption. intro. subst C'. apply cong_symmetry in H7. apply cong_identity in H7. subst A'. absurde. right. unfold Col. left. assumption. assumption. assert(exists C' , CongA A B C A' B' C' /\ OS A' B' C' P). apply angle_construction_1. assumption. assumption. ex_and H5 C'. exists C'. split. assumption. left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2