fact: Fixpoint sigma_add i v m := match m with | sigma_empty => match i with | xH => N sigma_empty (Some v) sigma_empty | xO i => N (sigma_add i v sigma_empty) None sigma_empty | xI i => N sigma_empty None (sigma_add i v sigma_empty) end | N l o r => match i with | xH => N l (Some v) r | xO i => N (sigma_add i v l) o r | xI i => N l o (sigma_add i v r) end end.
imports: BinNums comparisons