proposition: Lemma cong_cop_perp_bisect : forall P Q A B, P <> Q -> A <> B -> Coplanar P Q A B -> Cong A P B P -> Cong A Q B Q -> Perp_bisect P Q A B.
proof: Proof. intros. apply perp_bisect_equiv_def. unfold Perp_bisect_bis. elim (midpoint_existence A B). intros I HI. exists I. split;try assumption. assert (Per P I A) by (exists B; split; Cong). show_distinct A I. unfold Midpoint in *. spliter. treat_equalities. intuition. show_distinct B I. unfold Midpoint in *. spliter. treat_equalities. intuition. induction(eq_dec_points P I). subst. eapply l8_13_2;Col. exists Q. exists B;repeat split;Col. unfold Per. exists A. split. Midpoint. Cong. eapply l8_13_2. assumption. assumption. apply col_permutation_2. apply cop_per2__col with A; Col. destruct(col_dec B A P). exists I. left. split; ColR. apply coplanar_perm_12, col_cop__cop with B; Col; Cop. exists B; split; Cong. apply midpoint_col;auto. exists P. exists A. repeat split;Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2