fact: Definition succ x := match x with | N0 wx => match w0_succ_c wx with | C0 r => N0 r | C1 r => N1 (WW one0 r) end | N1 wx => match w1_succ_c wx with | C0 r => N1 r | C1 r => N2 (WW one1 r) end | N2 wx => match w2_succ_c wx with | C0 r => N2 r | C1 r => N3 (WW one2 r) end | N3 wx => match w3_succ_c wx with | C0 r => N3 r | C1 r => N4 (WW one3 r) end | N4 wx => match w4_succ_c wx with | C0 r => N4 r | C1 r => N5 (WW one4 r) end | N5 wx => match w5_succ_c wx with | C0 r => N5 r | C1 r => N6 (WW one5 r) end | N6 wx => match w6_succ_c wx with | C0 r => N6 r | C1 r => N7 (WW one6 r) end | N7 wx => match w7_succ_c wx with | C0 r => N7 r | C1 r => N8 (WW one7 r) end | N8 wx => match w8_succ_c wx with | C0 r => N8 r | C1 r => N9 (WW one8 r) end | N9 wx => match w9_succ_c wx with | C0 r => N9 r | C1 r => N10 (WW one9 r) end | N10 wx => match w10_succ_c wx with | C0 r => N10 r | C1 r => N11 (WW one10 r) end | N11 wx => match w11_succ_c wx with | C0 r => N11 r | C1 r => N12 (WW one11 r) end | N12 wx => match w12_succ_c wx with | C0 r => N12 r | C1 r => Nn 0 (WW one12 r) end | Nn n wx => let op := make_op n in match op.(znz_succ_c) wx with | C0 r => Nn n r | C1 r => Nn (S n) (WW op.(znz_1) r) end end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1