proposition: Lemma perp_bisect_equiv_def : forall P Q A B, Perp_bisect P Q A B <-> Perp_bisect_bis P Q A B.
proof: Proof. intros; unfold Perp_bisect; unfold Perp_bisect_bis; unfold ReflectL; split. { intro H; destruct H as [[[X [HMid HCol]] HPerp] HDiff]. exists X; split; Midpoint. elim HPerp; clear HPerp; intro HPerp; [|exfalso;auto]. apply l8_14_2_1b_bis; Col; Perp. } { intro H; destruct H as [I [HPerp HMid]]. assert_diffs; split; Col. split; try (left; apply l8_14_2_1a with I); Perp. exists I; split; Midpoint. unfold Perp_at in *; spliter; Col. } Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2