proposition: Lemma perp_bisect_perp : forall P Q A B, Perp_bisect P Q A B -> Perp P Q A B.
proof: Proof. intros. apply perp_bisect_equiv_def in H. unfold Perp_bisect_bis in *. decompose [and ex] H;clear H. unfold Perp. exists x. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2