proposition: Lemma cong2_cop2_onc3__eq : forall O P X 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 -> Cong X A X B -> Cong X A X C -> Coplanar A B C X -> X = O.
proof: Proof. intros O P X A B C HAB HAC HBC HAOn HBOn HCOn HCop HCong1 HCong2 HCop1. destruct (midpoint_existence A B) as [M1 HM1]. destruct (midpoint_existence A C) as [M2 HM2]. assert (HNCol : ~ Col C A B) by (apply (onc3__ncol O P); auto). destruct (l10_15 A B M1 C) as [P1 [HPerp1 HOS1]]; Col. destruct (l10_15 A C M2 B) as [P2 [HPerp2 HOS2]]; Col. assert (HColX1 : Col M1 P1 X). apply (cop_mid_onc2_perp__col X A A B); Circle; Perp. apply coplanar_perm_12, coplanar_trans_1 with C; Cop. assert (HColO1 : Col M1 P1 O). apply (cop_mid_onc2_perp__col O P A B); Perp. apply coplanar_perm_12, coplanar_trans_1 with C; Cop. apply not_col_permutation_3 in HNCol. assert (HColX2 : Col M2 P2 X). apply (cop_mid_onc2_perp__col X A A C); Circle; Perp. apply coplanar_perm_12, coplanar_trans_1 with B; Cop. assert (HColO2 : Col M2 P2 O). apply (cop_mid_onc2_perp__col O P A C); Perp. apply coplanar_perm_12, coplanar_trans_1 with B; Cop. assert_diffs. destruct (col_dec M1 P1 M2); [apply (l6_21 M2 P2 M1 P1)|apply (l6_21 M1 P1 M2 P2)]; Col. intro. apply HBC. destruct (eq_dec_points M1 M2). apply (symmetric_point_uniqueness A M1); subst; trivial. apply l10_2_uniqueness_spec with M1 P1 A. split; Perp; exists M1; Col. split. exists M2; auto. left. apply perp_col2 with P2 M2; Perp; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel