proposition: Lemma perp_bisect_is_on_perp_bisect : forall A B C P, Is_on_perp_bisect P A B -> Is_on_perp_bisect P B C -> Is_on_perp_bisect P A C.
proof: Proof. intros. unfold Is_on_perp_bisect in *. CongR. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2