proposition: Lemma perp_dec : forall A B C D, Perp A B C D \/ ~ Perp A B C D.
proof: Proof. intros. induction (col_dec A B C). induction (perp_in_dec C A B C D). left. apply l8_14_2_1a with C;auto. right. intro. apply H0. clear H0. apply perp_in_right_comm. apply (l8_15_1 A B D C). apply perp_distinct in H1. intuition. apply perp_right_comm;assumption. elim (l8_18_existence A B C H); intros P HP. spliter. induction (eq_dec_points C D). subst. right. intro. assert (A <> B /\ D <> D) by (apply perp_distinct;assumption). intuition. induction (col_dec P C D). left. assert (A <> B /\ C <> P) by (apply perp_distinct;assumption). spliter. apply perp_col1 with P;Col. right. intro. apply H3. apply col_permutation_2, cop_perp2__col with A B; [Cop|apply perp_sym;assumption..]. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles