proposition: Lemma two_sides_dec : forall A B C D, TS A B C D \/ ~ TS A B C D.
proof: Proof. intros. destruct (col_dec C A B). right; intros []; contradiction. destruct (col_dec D A B) as [|HNCol]. right; intros [HN []]; contradiction. destruct (l8_18_existence A B C) as [C0 [HCol1 HPerp1]]; Col. destruct (l8_18_existence A B D) as [D0 [HCol2 HPerp2]]; Col. assert_diffs. destruct (midpoint_existence C0 D0) as [M]. assert (Col M A B). destruct (eq_dec_points C0 D0); [treat_equalities; Col|ColR]. destruct (l6_11_existence D0 C0 C D) as [D' []]; auto. destruct (bet_dec C M D') as [|HNBet]. { left; apply l9_2, l9_5 with D' D0; Col. repeat split; auto. intro; apply HNCol; ColR. exists M; split; Between. } right; intro HTS. apply HNBet. assert (HTS1 : TS A B D' C). apply l9_5 with D D0; [apply l9_2|Col|apply l6_6]; assumption. destruct (eq_dec_points C0 D0). { treat_equalities. assert (Col M C D) by (apply cop_perp2__col with A B; Perp; Cop). destruct (distinct A B M); auto. - apply col_two_sides_bet with A. ColR. apply invert_two_sides, col_two_sides with B; Col; apply l9_2, HTS1. - apply col_two_sides_bet with B. ColR. apply invert_two_sides, col_two_sides with A; Col. apply l9_2, invert_two_sides, HTS1. } destruct HTS1 as [HNCol' [_ [M' []]]]. destruct (l8_22 C0 D0 C D' M') as [_ []]; Between; Cong; Col. apply perp_per_1, perp_col2 with A B; auto. assert_diffs; apply per_col with D; Col; apply perp_per_1, perp_col2 with A B; auto. ColR. replace M with M'; Between. apply (l7_17 C0 D0); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar