proposition: Lemma perp_in_dec : forall X A B C D, Perp_at X A B C D \/ ~ Perp_at X A B C D.
proof: Proof. intros. unfold Perp_at. elim (eq_dec_points A B);intro; elim (eq_dec_points C D);intro; elim (col_dec X A B);intro; elim (col_dec X C D);intro; try tauto. elim (eq_dec_points B X);intro; elim (eq_dec_points D X);intro;subst;treat_equalities. elim (per_dec A X C);intro. left;repeat split;Col;intros; apply col_col_per_per with A C;Col. right;intro;spliter;apply H3;apply H8;Col. elim (per_dec A X D);intro. left;repeat split;Col;intros; apply col_col_per_per with A D;ColR. right;intro;spliter;apply H3;apply H9;Col. elim (per_dec B X C);intro. left;repeat split;Col;intros; apply col_col_per_per with B C;ColR. right;intro;spliter;apply H4;apply H9;Col. elim (per_dec B X D);intro. left;repeat split;Col;intros; apply col_col_per_per with B D;ColR. right;intro;spliter;apply H5;apply H10;Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR