proposition: Lemma angle_construction_3 : forall A B C A' B', A <> B -> C <> B -> A' <> B' -> exists C', CongA A B C A' B' C'.
proof: Proof. intros. assert(exists P, ~Col A' B' P). eapply not_col_exists. assumption. ex_and H2 P. induction (eq_dec_points A C). subst C. exists A'. apply conga_trivial_1; assumption. assert(exists C', CongA A B C A' B' C' /\ (OS A' B' C' P \/ Col A' B' C')). apply angle_construction_2. assumption. assumption. auto. assumption. assumption. ex_and H4 C'. exists C'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2