proposition: Lemma perp_not_par : forall A B X Y, Perp A B X Y -> ~ Par A B X Y.
proof: Proof. intros. assert(HH:=H). unfold Perp in HH. ex_and HH P. intro. induction H1. apply H1. exists P. apply perp_in_col in H0. spliter. split; Col. spliter. induction(eq_dec_points A Y). subst Y. assert(P = A). eapply (l8_14_2_1b P A B X A); Col. subst P. apply perp_in_comm in H0. apply perp_in_per in H0. assert(~ Col B A X). eapply(per_not_col). auto. auto. assumption. apply H5. Col. apply(l8_16_1 A B X A Y); Col. ColR. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles