fact: Fixpoint natmap_fold_raw {A B} (f : nat → A → B → B) (j : nat) (d : B) (l : natmap_raw A) : B := match l with | [] => d | mx :: l => natmap_fold_raw f (S j) match mx with Some x => f j x d | None => d end l end.
imports: stdpp(fin_maps mapset) stdpp(options)