proposition: Lemma extend_n2f n f x (h:x<n) : n2f (extend_ok f h) = f (n2f h).
proof: Proof. generalize (extend_ok f h). unfold extend in *. break_dec h. intros h'. rewrite <- n2f_f2n. now apply n2f_ext. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec