proposition: Lemma not_par_two_sides : forall A B C D I, C <> D -> Col A B I -> Col C D I -> ~ Col A B C -> exists X, exists Y, Col C D X /\ Col C D Y /\ TS A B X Y.
proof: Proof. intros A B C D I HCD HCol1 HCol2 HNC. assert (HX : exists X, Col C D X /\ I <> X) by (exists C; split; try intro; treat_equalities; Col). destruct HX as [X [HCol3 HIX]]. destruct (symmetric_point_construction X I) as [Y HMid]. exists X; exists Y; assert_diffs; assert_cols; repeat split; try ColR. intro; apply HIX, l6_21 with A B C D; Col. intro; absurd (I = Y); [auto|apply l6_21 with A B C D; ColR]. exists I; unfold Midpoint in HMid; spliter; split; Col; Between. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity