proposition: Lemma perp_bisect_cong2 : forall P Q A B, Perp_bisect P Q A B -> Cong A P B P /\ Cong A Q B Q.
proof: Proof. intros. split. eauto using perp_bisect_cong_1. eauto using perp_bisect_cong_2. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2