proposition: Lemma perp_bisect_sym_3 : forall A B C D, Perp_bisect A B C D -> Perp_bisect B A D C.
proof: Proof. intros. apply perp_bisect_sym_1. apply perp_bisect_sym_2. trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2