proposition: Lemma cong_cop_mid_perp__col : forall A B M P X, Coplanar A B X P -> Cong A X B X -> Midpoint M A B -> Perp A B P M -> Col M P X.
proof: Proof. intros. apply (cop__cong_on_bissect A B); Cong. apply l8_15_1; Col. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity