proposition: Lemma PlgEquivDef: forall A B C D, (A <> C \/ B <> D) -> ((exists M, OnCircle C M A /\ OnCircle D M B /\ Bet C M A /\ Bet D M B) <-> Plg A B C D).
proof: Proof. intros. split. - intros. unfold OnCircle in *. split. assumption. ex_and H0 M. exists M. split. { unfold Midpoint. split;Between. Cong. } { unfold Midpoint in *. split;Between. Cong. } - intros. unfold OnCircle in *. ex_and H0 M. ex_and H1 M1. unfold Midpoint in *. exists M1. split;Cong. split;[Cong|Between]. Qed.
imports: GeoCoq.Tarski_dev.Annexes.perp_bisect