proposition: Lemma perp_bisect_existence_cop : forall A B C, A <> B -> exists P, exists Q, Perp_bisect P Q A B /\ Coplanar A B C P /\ Coplanar A B C Q.
proof: Proof. intros A B C HDiff. destruct (midpoint_existence A B) as [M HM]. destruct (ex_perp_cop A B M C) as [Q [HQ HCop]]; auto. exists M; exists Q; unfold Perp_bisect. repeat split; Perp; [|Cop]. exists M; split; [Midpoint|Col]. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2