proposition: Lemma cop_not_par_other_side : forall A B C D I P, C <> D -> Col A B I -> Col C D I -> ~ Col A B C -> ~ Col A B P -> Coplanar A B C P -> exists Q, Col C D Q /\ TS A B P Q.
proof: Proof. intros A B C D I P HCD HCol1 HCol2 HNC1 HNC2 HCop. destruct (not_par_two_sides A B C D I HCD HCol1 HCol2 HNC1) as [X [Y [HCol3 [HCol4 HTS]]]]. assert (Coplanar A B P X). apply coplanar_trans_1 with C; [Col|Cop|]. exists I; right; right; split; ColR. elim (two_sides_dec A B P X); intro HOS; [exists X; Col|]. assert_diffs; apply cop_nts__os in HOS; Col; [|intro; unfold TS in HTS; intuition]. exists Y; split; Col. apply l9_8_2 with X; [|apply one_side_symmetry]; Col. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity