proposition: Lemma one_or_two_sides_aux : forall A B C D X, ~ Col C A B -> ~ Col D A B -> Col A C X -> Col B D X -> TS A B C D \/ OS A B C D.
proof: Proof. intros. assert_diffs. assert (A <> X) by (intro; subst; Col). assert (B <> X) by (intro; subst; Col). assert (~ Col X A B) by (intro; apply H; ColR). destruct H1 as [|[|]]; destruct H2 as [|[|]]. - right. apply one_side_transitivity with X. apply out_one_side; Col. apply bet_out; auto. apply invert_one_side, out_one_side; Col. apply l6_6, bet_out; auto. - right. apply one_side_transitivity with X. apply out_one_side; Col. apply bet_out; auto. apply invert_one_side, out_one_side; Col. apply bet_out; Between. - left. apply l9_8_2 with X. repeat split; Col. exists B; split; Col. apply out_one_side; Col. apply l6_6, bet_out; auto. - right. apply one_side_transitivity with X. apply out_one_side; Col. apply l6_6, bet_out; Between. apply invert_one_side, out_one_side; Col. apply l6_6, bet_out; auto. - right. apply one_side_transitivity with X. apply out_one_side; Col. apply l6_6, bet_out; Between. apply invert_one_side, out_one_side; Col. apply bet_out; Between. - left. apply l9_8_2 with X. repeat split; Col. exists B; split; Col. apply out_one_side; Col. apply bet_out; Between. - left. apply l9_2, l9_8_2 with X. repeat split; Col. exists A; split; Col. apply invert_one_side, out_one_side; Col. apply l6_6, bet_out; auto. - left. apply l9_2, l9_8_2 with X. repeat split; Col. exists A; split; Col. apply invert_one_side, out_one_side; Col. apply bet_out; Between. - right. exists X; repeat split; Col. exists A; split; [Col|Between]. exists B; split; [Col|Between]. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar