proposition: Lemma cong_cop2_perp_bisect_col : forall A B C D E, Coplanar A C D E -> Coplanar B C D E -> Cong C D C E -> Perp_bisect A B D E -> Col A B C.
proof: Proof. intros A B C D E HCop1 HCop2 HCong1 HPerp. assert (HCong2 := HPerp); apply perp_bisect_cong2 in HCong2; destruct HCong2 as [HCong2 Hc]; clear Hc. apply perp_bisect_equiv_def in HPerp. destruct HPerp as [F [HPerp [HBet HCong3]]]. assert (HDE : D <> E) by (assert_diffs; auto). assert (HCol := HPerp); apply perp_in_col in HCol; destruct HCol as [HCol Hc]; clear Hc. apply l8_14_2_1a in HPerp. elim (eq_dec_points A C); intro; try (subst; Col). apply cop_perp2__col with D E; Perp; Cop. apply perp_bisect_perp; apply cong_cop_perp_bisect; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2