proposition: Lemma g_ge_id : forall i, g i >= i.
proof: Proof. induction i. lia. simpl. destruct (ch_min (H (S (g i)))). simpl. lia. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)