proposition: Lemma tree_points_onc_cop2 : forall O P Q, O <> P -> exists A B C, A <> B /\ A <> C /\ B <> C /\ OnCircle A O P /\ OnCircle B O P /\ OnCircle C O P /\ Coplanar A B C O /\ Coplanar A B C Q.
proof: Proof. intros O P Q HOP. destruct (eq_dec_points O Q). subst Q. destruct (tree_points_onc_cop O P HOP) as [A [B [C]]]; spliter. exists A, B, C; repeat split; auto. destruct (not_col_exists O Q) as [X HNCol]; auto. destruct (diam_points O P X) as [B [C [HBet [HCol []]]]]. destruct (l6_11_existence O O P Q) as [A []]; auto. exists A, B, C. assert (~ Col O A B) by (intro; unfold OnCircle in *; assert_diffs; apply HNCol; ColR). assert_diffs. repeat split; Circle. intro; subst; apply HNCol; ColR. exists B; left; split; Col. exists O; right; right; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel