proposition: Lemma natmap_push_pop {A} (m : natmap A) : natmap_push (m !! 0) (natmap_pop m) = m.
proof: Proof. apply map_eq. intros i. destruct i. - by rewrite lookup_natmap_push_O. - by rewrite lookup_natmap_push_S, lookup_natmap_pop. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)