proposition: Lemma G_is_classic_left_total : classic_left_total G.
proof: Proof. intro. elim x. exists a. exact G0. intros. destruct H. exists (next_elt x0). exact (GS H). Qed.
imports: Coq(ClassicalChoice) CoLoR(RelUtil LogicUtil)