fact: Fixpoint upd_nat {A:Type} (l:list A) (n:nat) (a:A) : option (list A) := match l with | nil => None | x::q => match n with | O => Some (a::q) | S p => match upd_nat q p a with | None => None | Some q' => Some (x::q') end end end.
imports: ZArith List MSetPositive