proposition: Lemma col_2_le_or_ge : forall O E E' A B, ~ Col O E E' -> Col O E A -> Col O E B -> LeP O E E' A B \/ LeP O E E' B A.
proof: Proof. intros O E E' A B HNC HColA HColB. assert (HDiff1 : O <> E) by (assert_diffs; auto). elim (eq_dec_points A B); intro HDiff2; treat_equalities; [left; right; auto|]. destruct (diff_exists O E E' B A) as [D HD]; Col. assert (HColD : Col O E D) by (apply diff_ar2 in HD; unfold Ar2 in *; spliter; Col). assert (HDiff3 : O <> D) by (intro; treat_equalities; apply diff_null_eq in HD; intuition). apply col_pos_or_neg in HColD; auto. elim HColD; clear HColD; intro HNgD; [left; left; exists D; auto|]. destruct (diff_exists O E E' A B) as [MD HMD]; Col. right; left; exists MD; split; auto; apply opp_neg_pos with E' D; auto. apply diff_opp with B A; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod