proposition: Lemma perp_bisect_cong : forall A A1 B B1 C C1 O: Tpoint, ~ Col A B C -> Perp_bisect O A1 B C -> Perp_bisect O B1 A C -> Perp_bisect O C1 A B -> Cong A O B O -> Cong B O C O -> Cong A O C O.
proof: Proof. intros. apply (cong_transitivity A O B O C O); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2