proposition: Lemma cop__cong_on_bissect : forall A B M P X, Coplanar A B X P -> Midpoint M A B -> Perp_at M A B P M -> Cong X A X B -> Col M P X.
proof: Proof. intros. assert(X = M \/ ~ Col A B X /\ Perp_at M X M A B). assert_diffs; apply(cong_perp_or_mid A B M X); Cong. induction H3. treat_equalities; Col. spliter. apply perp_in_perp in H1. apply perp_in_perp in H4. assert_cols. apply(cop_perp2__col _ _ _ A B); Perp; Cop. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity