proposition: Lemma not_col_exists : forall A B, A<>B -> exists C, ~ Col A B C.
proof: Proof. intros. assert (T:=lower_dim_ex). induction T. induction H0. induction H0. induction (col_dec A B x). induction(col_dec A B x0). induction(col_dec A B x1). induction (eq_dec_points A x). assert (~(Col x x0 x1)) by (unfold Col; auto). treat_equalities; eCol. assert (Col A x x0) by eCol. assert (Col A x x1) by eCol. assert (Col A x0 x1) by eCol. assert (Col x x0 x1) by eCol. contradiction. exists x1; assumption. exists x0; assumption. exists x; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le