proposition: Lemma col2_dec : forall A B C D E F, (Col A B C /\ Col D E F) \/ ~ (Col A B C /\ Col D E F).
proof: Proof. intros A B C D E F. induction (col_dec A B C); induction (col_dec D E F); [left; split; assumption|right; intro Hc; induction Hc; auto..]. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel