fact: Definition pred x := match x with | N0 wx => match w0_pred_c wx with | C0 r => reduce_0 r | C1 r => zero end | N1 wx => match w1_pred_c wx with | C0 r => reduce_1 r | C1 r => zero end | N2 wx => match w2_pred_c wx with | C0 r => reduce_2 r | C1 r => zero end | N3 wx => match w3_pred_c wx with | C0 r => reduce_3 r | C1 r => zero end | N4 wx => match w4_pred_c wx with | C0 r => reduce_4 r | C1 r => zero end | N5 wx => match w5_pred_c wx with | C0 r => reduce_5 r | C1 r => zero end | N6 wx => match w6_pred_c wx with | C0 r => reduce_6 r | C1 r => zero end | N7 wx => match w7_pred_c wx with | C0 r => reduce_7 r | C1 r => zero end | N8 wx => match w8_pred_c wx with | C0 r => reduce_8 r | C1 r => zero end | N9 wx => match w9_pred_c wx with | C0 r => reduce_9 r | C1 r => zero end | N10 wx => match w10_pred_c wx with | C0 r => reduce_10 r | C1 r => zero end | N11 wx => match w11_pred_c wx with | C0 r => reduce_11 r | C1 r => zero end | N12 wx => match w12_pred_c wx with | C0 r => reduce_12 r | C1 r => zero end | Nn n wx => let op := make_op n in match op.(znz_pred_c) wx with | C0 r => reduce_n n r | C1 r => zero end end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1