proposition: Lemma mid2_onc4__eq : forall O P A B C D X, B <> C-> A <> B -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P -> Midpoint X A C -> Midpoint X B D -> X=O.
proof: Proof. intros O P A B C D X Hbc. intros. assert(HH:=mid_onc2__per O P A C X H0 H2 H4). assert(HP:=mid_onc2__per O P B D X H1 H3 H5). induction(eq_dec_points X O). auto. assert(Col A B X). apply(per2__col A B O X); Perp. unfold Midpoint in *. spliter. assert(Col B X D). apply bet_col; auto. assert(Col A X C). ColR. induction(eq_dec_points A X). subst X. treat_equalities. assert(OutCircleS D O P). apply(onc2_out__outcs O P A B D); auto. assert_diffs. unfold Out. split. auto. split. auto. left; Between. unfold OutCircleS in *. unfold Lt in *. spliter. unfold OnCircle in H3. apply False_ind. absurd (Cong O P O D);Cong. assert(Col A B C). ColR. assert(C = A \/ C = B). apply(line_circle_two_points O P A B C); Col. destruct H14. treat_equalities. intuition. treat_equalities. assert(A = D) by (apply (symmetric_point_uniqueness C X); split; Between; Cong). treat_equalities. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel