proposition: Lemma perp_bisect_sym_2 : forall P Q A B, Perp_bisect P Q A B -> Perp_bisect P Q B A.
proof: Proof. intros. apply perp_bisect_equiv_def in H. apply perp_bisect_equiv_def. unfold Perp_bisect_bis in *. elim H;intros. exists x. intuition; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2