proposition: Lemma cong_chord_cong_center1 : forall O P A B C D M N, A <> B -> C <> D -> M <> A -> N <> C -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P -> Col M A B -> Col N C D -> Per O M A -> Per O N C -> Cong A B C D -> Cong O N O M.
proof: Proof. intros. assert(Midpoint M A B). apply(onc2_per__mid O P A B M H H1 H3 H4 H7 H9). assert(Midpoint N C D). apply(onc2_per__mid O P C D N H0 H2 H5 H6 H8 H10). apply (cong_chord_cong_center O P A B C D M N); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel