proposition: Lemma g_neq : forall i j, g i < j < g (S i) -> f j <> a.
proof: Proof. intros i j hj e. assert (g (S i) <= j). simpl. destruct (ch_min (H (S (g i)))). simpl. intuition. lia. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)