proposition: Lemma g_complete : forall i, f i = a -> exists j, i = g j.
proof: Proof. intros i hi. assert (h : exists j, g j >= i). exists i. apply g_ge_id. exists (proj1_sig (ch_min h)). destruct (ch_min h). simpl. clear h. apply NNPP. intro. assert (h1 : i < g x). lia. destruct x. absurd (g 0 <= i). lia. simpl. destruct (ch_min (H 0)). simpl. intuition. assert (h2 : g x < i). apply NNPP. intro. cut (S x <= x). lia. intuition. absurd (f i = a). eapply g_neq. split. apply h2. hyp. hyp. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)