proposition: Lemma col_decG : forall A B C, ColG A B C \/ ~ ColG A B C.
proof: Proof. intros A B C; unfold ColG; induction (bet_decG A B C); induction (bet_decG B C A); induction (bet_decG C A B); tauto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le