proposition: Lemma median_planes_aux : (forall A B C P Q M, P <> Q -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q -> Midpoint M P Q -> Coplanar M A B C) -> median_planes_axiom.
proof: Proof. intros Haux A B C D P Q; intros. destruct (col_dec A B C) as [HCop|]; [apply col__coplanar, HCop|]. destruct (midpoint_existence P Q) as [M]. destruct (ex_ncol_cop2 A B C M) as [A1 [A2 [HCop1 [HCop2 HNCol1]]]]. assert (Cong A1 P A1 Q) by (apply (l11_60_aux A B C); assumption). assert (Cong A2 P A2 Q) by (apply (l11_60_aux A B C); assumption). apply coplanar_pseudo_trans with M A1 A2; eauto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv