proposition: Lemma circle_circle_os : forall A B C D I P, OnCircle I A B -> OnCircle I C D -> ~ Col A C I -> ~ Col A C P -> exists Z, OnCircle Z A B /\ OnCircle Z C D /\ OS A C P Z.
proof: Proof. intros A B C D I P HI1 HI2 HNCol1 HNCol2. destruct (l8_18_existence A C I) as [X []]; trivial. destruct (l10_15 A C X P) as [Z0 []]; trivial. assert_diffs. destruct (l6_11_existence X X I Z0) as [Z []]; auto. exists Z. assert (Perp A C X Z). assert_diffs; apply perp_sym, perp_col with Z0; Perp; Col. assert (OS A C P Z). apply one_side_transitivity with Z0; trivial. apply out_one_side_1 with X; [apply one_side_not_col124 with P| |apply l6_6]; trivial. clear dependent Z0. repeat split; auto. - apply cong_transitivity with A I; trivial. destruct (eq_dec_points A X). subst; assumption. apply l10_12 with X X; Cong; [apply perp_per_2|apply perp_per_1]; apply perp_left_comm, perp_col with C; auto. - apply cong_transitivity with C I; trivial. destruct (eq_dec_points C X). subst; assumption. apply l10_12 with X X; Cong; [apply perp_per_2|apply perp_per_1]; apply perp_left_comm, perp_col with A; Perp; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel