proposition: Lemma cong_chord_cong_center : forall O P A B C D M N, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P -> Midpoint M A B -> Midpoint N C D -> Cong A B C D -> Cong O N O M.
proof: Proof. intros. assert(Cong M B N D). apply cong_commutativity. eapply (cong_cong_half_1 _ _ A _ _ C); Midpoint. Cong. unfold Midpoint in *. unfold OnCircle in *. spliter. apply cong_commutativity. apply cong_symmetry. apply(l4_2 A M B O C N D O). unfold IFSC. repeat split; Cong. apply (cong_transitivity _ _ O P); Cong. apply (cong_transitivity _ _ O P); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel