fact: Definition mod_gt x y := match x, y with | N0 wx, N0 wy => reduce_0 (w0_mod_gt wx wy) | N0 wx, N1 wy => let wx':= GenBase.extend w0_op.(znz_0W) 0 wx in reduce_1 (w1_mod_gt wx' wy) | N0 wx, N2 wy => let wx':= GenBase.extend w0_op.(znz_0W) 1 wx in reduce_2 (w2_mod_gt wx' wy) | N0 wx, N3 wy => let wx':= GenBase.extend w0_op.(znz_0W) 2 wx in reduce_3 (w3_mod_gt wx' wy) | N0 wx, N4 wy => let wx':= GenBase.extend w0_op.(znz_0W) 3 wx in reduce_4 (w4_mod_gt wx' wy) | N0 wx, N5 wy => let wx':= GenBase.extend w0_op.(znz_0W) 4 wx in reduce_5 (w5_mod_gt wx' wy) | N0 wx, N6 wy => let wx':= GenBase.extend w0_op.(znz_0W) 5 wx in reduce_6 (w6_mod_gt wx' wy) | N0 wx, N7 wy => let wx':= GenBase.extend w0_op.(znz_0W) 6 wx in reduce_7 (w7_mod_gt wx' wy) | N0 wx, N8 wy => let wx':= GenBase.extend w0_op.(znz_0W) 7 wx in reduce_8 (w8_mod_gt wx' wy) | N0 wx, N9 wy => let wx':= GenBase.extend w0_op.(znz_0W) 8 wx in reduce_9 (w9_mod_gt wx' wy) | N0 wx, N10 wy => let wx':= GenBase.extend w0_op.(znz_0W) 9 wx in reduce_10 (w10_mod_gt wx' wy) | N0 wx, N11 wy => let wx':= GenBase.extend w0_op.(znz_0W) 10 wx in reduce_11 (w11_mod_gt wx' wy) | N0 wx, N12 wy => let wx':= GenBase.extend w0_op.(znz_0W) 11 wx in reduce_12 (w12_mod_gt wx' wy) | N0 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w0_op.(znz_0W) 12 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N1 wx, N0 wy => reduce_0 (w0_modn1 1 wx wy) | N1 wx, N1 wy => reduce_1 (w1_mod_gt wx wy) | N1 wx, N2 wy => let wx':= GenBase.extend w1_op.(znz_0W) 0 wx in reduce_2 (w2_mod_gt wx' wy) | N1 wx, N3 wy => let wx':= GenBase.extend w1_op.(znz_0W) 1 wx in reduce_3 (w3_mod_gt wx' wy) | N1 wx, N4 wy => let wx':= GenBase.extend w1_op.(znz_0W) 2 wx in reduce_4 (w4_mod_gt wx' wy) | N1 wx, N5 wy => let wx':= GenBase.extend w1_op.(znz_0W) 3 wx in reduce_5 (w5_mod_gt wx' wy) | N1 wx, N6 wy => let wx':= GenBase.extend w1_op.(znz_0W) 4 wx in reduce_6 (w6_mod_gt wx' wy) | N1 wx, N7 wy => let wx':= GenBase.extend w1_op.(znz_0W) 5 wx in reduce_7 (w7_mod_gt wx' wy) | N1 wx, N8 wy => let wx':= GenBase.extend w1_op.(znz_0W) 6 wx in reduce_8 (w8_mod_gt wx' wy) | N1 wx, N9 wy => let wx':= GenBase.extend w1_op.(znz_0W) 7 wx in reduce_9 (w9_mod_gt wx' wy) | N1 wx, N10 wy => let wx':= GenBase.extend w1_op.(znz_0W) 8 wx in reduce_10 (w10_mod_gt wx' wy) | N1 wx, N11 wy => let wx':= GenBase.extend w1_op.(znz_0W) 9 wx in reduce_11 (w11_mod_gt wx' wy) | N1 wx, N12 wy => let wx':= GenBase.extend w1_op.(znz_0W) 10 wx in reduce_12 (w12_mod_gt wx' wy) | N1 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w1_op.(znz_0W) 11 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N2 wx, N0 wy => reduce_0 (w0_modn1 2 wx wy) | N2 wx, N1 wy => reduce_1 (w1_modn1 1 wx wy) | N2 wx, N2 wy => reduce_2 (w2_mod_gt wx wy) | N2 wx, N3 wy => let wx':= GenBase.extend w2_op.(znz_0W) 0 wx in reduce_3 (w3_mod_gt wx' wy) | N2 wx, N4 wy => let wx':= GenBase.extend w2_op.(znz_0W) 1 wx in reduce_4 (w4_mod_gt wx' wy) | N2 wx, N5 wy => let wx':= GenBase.extend w2_op.(znz_0W) 2 wx in reduce_5 (w5_mod_gt wx' wy) | N2 wx, N6 wy => let wx':= GenBase.extend w2_op.(znz_0W) 3 wx in reduce_6 (w6_mod_gt wx' wy) | N2 wx, N7 wy => let wx':= GenBase.extend w2_op.(znz_0W) 4 wx in reduce_7 (w7_mod_gt wx' wy) | N2 wx, N8 wy => let wx':= GenBase.extend w2_op.(znz_0W) 5 wx in reduce_8 (w8_mod_gt wx' wy) | N2 wx, N9 wy => let wx':= GenBase.extend w2_op.(znz_0W) 6 wx in reduce_9 (w9_mod_gt wx' wy) | N2 wx, N10 wy => let wx':= GenBase.extend w2_op.(znz_0W) 7 wx in reduce_10 (w10_mod_gt wx' wy) | N2 wx, N11 wy => let wx':= GenBase.extend w2_op.(znz_0W) 8 wx in reduce_11 (w11_mod_gt wx' wy) | N2 wx, N12 wy => let wx':= GenBase.extend w2_op.(znz_0W) 9 wx in reduce_12 (w12_mod_gt wx' wy) | N2 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w2_op.(znz_0W) 10 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N3 wx, N0 wy => reduce_0 (w0_modn1 3 wx wy) | N3 wx, N1 wy => reduce_1 (w1_modn1 2 wx wy) | N3 wx, N2 wy => reduce_2 (w2_modn1 1 wx wy) | N3 wx, N3 wy => reduce_3 (w3_mod_gt wx wy) | N3 wx, N4 wy => let wx':= GenBase.extend w3_op.(znz_0W) 0 wx in reduce_4 (w4_mod_gt wx' wy) | N3 wx, N5 wy => let wx':= GenBase.extend w3_op.(znz_0W) 1 wx in reduce_5 (w5_mod_gt wx' wy) | N3 wx, N6 wy => let wx':= GenBase.extend w3_op.(znz_0W) 2 wx in reduce_6 (w6_mod_gt wx' wy) | N3 wx, N7 wy => let wx':= GenBase.extend w3_op.(znz_0W) 3 wx in reduce_7 (w7_mod_gt wx' wy) | N3 wx, N8 wy => let wx':= GenBase.extend w3_op.(znz_0W) 4 wx in reduce_8 (w8_mod_gt wx' wy) | N3 wx, N9 wy => let wx':= GenBase.extend w3_op.(znz_0W) 5 wx in reduce_9 (w9_mod_gt wx' wy) | N3 wx, N10 wy => let wx':= GenBase.extend w3_op.(znz_0W) 6 wx in reduce_10 (w10_mod_gt wx' wy) | N3 wx, N11 wy => let wx':= GenBase.extend w3_op.(znz_0W) 7 wx in reduce_11 (w11_mod_gt wx' wy) | N3 wx, N12 wy => let wx':= GenBase.extend w3_op.(znz_0W) 8 wx in reduce_12 (w12_mod_gt wx' wy) | N3 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w3_op.(znz_0W) 9 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N4 wx, N0 wy => reduce_0 (w0_modn1 4 wx wy) | N4 wx, N1 wy => reduce_1 (w1_modn1 3 wx wy) | N4 wx, N2 wy => reduce_2 (w2_modn1 2 wx wy) | N4 wx, N3 wy => reduce_3 (w3_modn1 1 wx wy) | N4 wx, N4 wy => reduce_4 (w4_mod_gt wx wy) | N4 wx, N5 wy => let wx':= GenBase.extend w4_op.(znz_0W) 0 wx in reduce_5 (w5_mod_gt wx' wy) | N4 wx, N6 wy => let wx':= GenBase.extend w4_op.(znz_0W) 1 wx in reduce_6 (w6_mod_gt wx' wy) | N4 wx, N7 wy => let wx':= GenBase.extend w4_op.(znz_0W) 2 wx in reduce_7 (w7_mod_gt wx' wy) | N4 wx, N8 wy => let wx':= GenBase.extend w4_op.(znz_0W) 3 wx in reduce_8 (w8_mod_gt wx' wy) | N4 wx, N9 wy => let wx':= GenBase.extend w4_op.(znz_0W) 4 wx in reduce_9 (w9_mod_gt wx' wy) | N4 wx, N10 wy => let wx':= GenBase.extend w4_op.(znz_0W) 5 wx in reduce_10 (w10_mod_gt wx' wy) | N4 wx, N11 wy => let wx':= GenBase.extend w4_op.(znz_0W) 6 wx in reduce_11 (w11_mod_gt wx' wy) | N4 wx, N12 wy => let wx':= GenBase.extend w4_op.(znz_0W) 7 wx in reduce_12 (w12_mod_gt wx' wy) | N4 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w4_op.(znz_0W) 8 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N5 wx, N0 wy => reduce_0 (w0_modn1 5 wx wy) | N5 wx, N1 wy => reduce_1 (w1_modn1 4 wx wy) | N5 wx, N2 wy => reduce_2 (w2_modn1 3 wx wy) | N5 wx, N3 wy => reduce_3 (w3_modn1 2 wx wy) | N5 wx, N4 wy => reduce_4 (w4_modn1 1 wx wy) | N5 wx, N5 wy => reduce_5 (w5_mod_gt wx wy) | N5 wx, N6 wy => let wx':= GenBase.extend w5_op.(znz_0W) 0 wx in reduce_6 (w6_mod_gt wx' wy) | N5 wx, N7 wy => let wx':= GenBase.extend w5_op.(znz_0W) 1 wx in reduce_7 (w7_mod_gt wx' wy) | N5 wx, N8 wy => let wx':= GenBase.extend w5_op.(znz_0W) 2 wx in reduce_8 (w8_mod_gt wx' wy) | N5 wx, N9 wy => let wx':= GenBase.extend w5_op.(znz_0W) 3 wx in reduce_9 (w9_mod_gt wx' wy) | N5 wx, N10 wy => let wx':= GenBase.extend w5_op.(znz_0W) 4 wx in reduce_10 (w10_mod_gt wx' wy) | N5 wx, N11 wy => let wx':= GenBase.extend w5_op.(znz_0W) 5 wx in reduce_11 (w11_mod_gt wx' wy) | N5 wx, N12 wy => let wx':= GenBase.extend w5_op.(znz_0W) 6 wx in reduce_12 (w12_mod_gt wx' wy) | N5 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w5_op.(znz_0W) 7 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N6 wx, N0 wy => reduce_0 (w0_modn1 6 wx wy) | N6 wx, N1 wy => reduce_1 (w1_modn1 5 wx wy) | N6 wx, N2 wy => reduce_2 (w2_modn1 4 wx wy) | N6 wx, N3 wy => reduce_3 (w3_modn1 3 wx wy) | N6 wx, N4 wy => reduce_4 (w4_modn1 2 wx wy) | N6 wx, N5 wy => reduce_5 (w5_modn1 1 wx wy) | N6 wx, N6 wy => reduce_6 (w6_mod_gt wx wy) | N6 wx, N7 wy => let wx':= GenBase.extend w6_op.(znz_0W) 0 wx in reduce_7 (w7_mod_gt wx' wy) | N6 wx, N8 wy => let wx':= GenBase.extend w6_op.(znz_0W) 1 wx in reduce_8 (w8_mod_gt wx' wy) | N6 wx, N9 wy => let wx':= GenBase.extend w6_op.(znz_0W) 2 wx in reduce_9 (w9_mod_gt wx' wy) | N6 wx, N10 wy => let wx':= GenBase.extend w6_op.(znz_0W) 3 wx in reduce_10 (w10_mod_gt wx' wy) | N6 wx, N11 wy => let wx':= GenBase.extend w6_op.(znz_0W) 4 wx in reduce_11 (w11_mod_gt wx' wy) | N6 wx, N12 wy => let wx':= GenBase.extend w6_op.(znz_0W) 5 wx in reduce_12 (w12_mod_gt wx' wy) | N6 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w6_op.(znz_0W) 6 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N7 wx, N0 wy => reduce_0 (w0_modn1 7 wx wy) | N7 wx, N1 wy => reduce_1 (w1_modn1 6 wx wy) | N7 wx, N2 wy => reduce_2 (w2_modn1 5 wx wy) | N7 wx, N3 wy => reduce_3 (w3_modn1 4 wx wy) | N7 wx, N4 wy => reduce_4 (w4_modn1 3 wx wy) | N7 wx, N5 wy => reduce_5 (w5_modn1 2 wx wy) | N7 wx, N6 wy => reduce_6 (w6_modn1 1 wx wy) | N7 wx, N7 wy => reduce_7 (w7_mod_gt wx wy) | N7 wx, N8 wy => let wx':= GenBase.extend w7_op.(znz_0W) 0 wx in reduce_8 (w8_mod_gt wx' wy) | N7 wx, N9 wy => let wx':= GenBase.extend w7_op.(znz_0W) 1 wx in reduce_9 (w9_mod_gt wx' wy) | N7 wx, N10 wy => let wx':= GenBase.extend w7_op.(znz_0W) 2 wx in reduce_10 (w10_mod_gt wx' wy) | N7 wx, N11 wy => let wx':= GenBase.extend w7_op.(znz_0W) 3 wx in reduce_11 (w11_mod_gt wx' wy) | N7 wx, N12 wy => let wx':= GenBase.extend w7_op.(znz_0W) 4 wx in reduce_12 (w12_mod_gt wx' wy) | N7 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w7_op.(znz_0W) 5 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N8 wx, N0 wy => reduce_0 (w0_modn1 8 wx wy) | N8 wx, N1 wy => reduce_1 (w1_modn1 7 wx wy) | N8 wx, N2 wy => reduce_2 (w2_modn1 6 wx wy) | N8 wx, N3 wy => reduce_3 (w3_modn1 5 wx wy) | N8 wx, N4 wy => reduce_4 (w4_modn1 4 wx wy) | N8 wx, N5 wy => reduce_5 (w5_modn1 3 wx wy) | N8 wx, N6 wy => reduce_6 (w6_modn1 2 wx wy) | N8 wx, N7 wy => reduce_7 (w7_modn1 1 wx wy) | N8 wx, N8 wy => reduce_8 (w8_mod_gt wx wy) | N8 wx, N9 wy => let wx':= GenBase.extend w8_op.(znz_0W) 0 wx in reduce_9 (w9_mod_gt wx' wy) | N8 wx, N10 wy => let wx':= GenBase.extend w8_op.(znz_0W) 1 wx in reduce_10 (w10_mod_gt wx' wy) | N8 wx, N11 wy => let wx':= GenBase.extend w8_op.(znz_0W) 2 wx in reduce_11 (w11_mod_gt wx' wy) | N8 wx, N12 wy => let wx':= GenBase.extend w8_op.(znz_0W) 3 wx in reduce_12 (w12_mod_gt wx' wy) | N8 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w8_op.(znz_0W) 4 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N9 wx, N0 wy => reduce_0 (w0_modn1 9 wx wy) | N9 wx, N1 wy => reduce_1 (w1_modn1 8 wx wy) | N9 wx, N2 wy => reduce_2 (w2_modn1 7 wx wy) | N9 wx, N3 wy => reduce_3 (w3_modn1 6 wx wy) | N9 wx, N4 wy => reduce_4 (w4_modn1 5 wx wy) | N9 wx, N5 wy => reduce_5 (w5_modn1 4 wx wy) | N9 wx, N6 wy => reduce_6 (w6_modn1 3 wx wy) | N9 wx, N7 wy => reduce_7 (w7_modn1 2 wx wy) | N9 wx, N8 wy => reduce_8 (w8_modn1 1 wx wy) | N9 wx, N9 wy => reduce_9 (w9_mod_gt wx wy) | N9 wx, N10 wy => let wx':= GenBase.extend w9_op.(znz_0W) 0 wx in reduce_10 (w10_mod_gt wx' wy) | N9 wx, N11 wy => let wx':= GenBase.extend w9_op.(znz_0W) 1 wx in reduce_11 (w11_mod_gt wx' wy) | N9 wx, N12 wy => let wx':= GenBase.extend w9_op.(znz_0W) 2 wx in reduce_12 (w12_mod_gt wx' wy) | N9 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w9_op.(znz_0W) 3 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N10 wx, N0 wy => reduce_0 (w0_modn1 10 wx wy) | N10 wx, N1 wy => reduce_1 (w1_modn1 9 wx wy) | N10 wx, N2 wy => reduce_2 (w2_modn1 8 wx wy) | N10 wx, N3 wy => reduce_3 (w3_modn1 7 wx wy) | N10 wx, N4 wy => reduce_4 (w4_modn1 6 wx wy) | N10 wx, N5 wy => reduce_5 (w5_modn1 5 wx wy) | N10 wx, N6 wy => reduce_6 (w6_modn1 4 wx wy) | N10 wx, N7 wy => reduce_7 (w7_modn1 3 wx wy) | N10 wx, N8 wy => reduce_8 (w8_modn1 2 wx wy) | N10 wx, N9 wy => reduce_9 (w9_modn1 1 wx wy) | N10 wx, N10 wy => reduce_10 (w10_mod_gt wx wy) | N10 wx, N11 wy => let wx':= GenBase.extend w10_op.(znz_0W) 0 wx in reduce_11 (w11_mod_gt wx' wy) | N10 wx, N12 wy => let wx':= GenBase.extend w10_op.(znz_0W) 1 wx in reduce_12 (w12_mod_gt wx' wy) | N10 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w10_op.(znz_0W) 2 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N11 wx, N0 wy => reduce_0 (w0_modn1 11 wx wy) | N11 wx, N1 wy => reduce_1 (w1_modn1 10 wx wy) | N11 wx, N2 wy => reduce_2 (w2_modn1 9 wx wy) | N11 wx, N3 wy => reduce_3 (w3_modn1 8 wx wy) | N11 wx, N4 wy => reduce_4 (w4_modn1 7 wx wy) | N11 wx, N5 wy => reduce_5 (w5_modn1 6 wx wy) | N11 wx, N6 wy => reduce_6 (w6_modn1 5 wx wy) | N11 wx, N7 wy => reduce_7 (w7_modn1 4 wx wy) | N11 wx, N8 wy => reduce_8 (w8_modn1 3 wx wy) | N11 wx, N9 wy => reduce_9 (w9_modn1 2 wx wy) | N11 wx, N10 wy => reduce_10 (w10_modn1 1 wx wy) | N11 wx, N11 wy => reduce_11 (w11_mod_gt wx wy) | N11 wx, N12 wy => let wx':= GenBase.extend w11_op.(znz_0W) 0 wx in reduce_12 (w12_mod_gt wx' wy) | N11 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w11_op.(znz_0W) 1 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N12 wx, N0 wy => reduce_0 (w0_modn1 12 wx wy) | N12 wx, N1 wy => reduce_1 (w1_modn1 11 wx wy) | N12 wx, N2 wy => reduce_2 (w2_modn1 10 wx wy) | N12 wx, N3 wy => reduce_3 (w3_modn1 9 wx wy) | N12 wx, N4 wy => reduce_4 (w4_modn1 8 wx wy) | N12 wx, N5 wy => reduce_5 (w5_modn1 7 wx wy) | N12 wx, N6 wy => reduce_6 (w6_modn1 6 wx wy) | N12 wx, N7 wy => reduce_7 (w7_modn1 5 wx wy) | N12 wx, N8 wy => reduce_8 (w8_modn1 4 wx wy) | N12 wx, N9 wy => reduce_9 (w9_modn1 3 wx wy) | N12 wx, N10 wy => reduce_10 (w10_modn1 2 wx wy) | N12 wx, N11 wy => reduce_11 (w11_modn1 1 wx wy) | N12 wx, N12 wy => reduce_12 (w12_mod_gt wx wy) | N12 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w12_op.(znz_0W) 0 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | Nn n wx, N0 wy => let wy':= GenBase.extend w0_op.(znz_0W) 11 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N1 wy => let wy':= GenBase.extend w1_op.(znz_0W) 10 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N2 wy => let wy':= GenBase.extend w2_op.(znz_0W) 9 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N3 wy => let wy':= GenBase.extend w3_op.(znz_0W) 8 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N4 wy => let wy':= GenBase.extend w4_op.(znz_0W) 7 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N5 wy => let wy':= GenBase.extend w5_op.(znz_0W) 6 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N6 wy => let wy':= GenBase.extend w6_op.(znz_0W) 5 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N7 wy => let wy':= GenBase.extend w7_op.(znz_0W) 4 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N8 wy => let wy':= GenBase.extend w8_op.(znz_0W) 3 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N9 wy => let wy':= GenBase.extend w9_op.(znz_0W) 2 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N10 wy => let wy':= GenBase.extend w10_op.(znz_0W) 1 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N11 wy => let wy':= GenBase.extend w11_op.(znz_0W) 0 wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, N12 wy => let wy':= wy in reduce_12 (w12_modn1 (S n) wx wy') | Nn n wx, Nn m wy => match extend_to_max w12 n m wx wy with | inl wx' => reduce_n m ((make_op m).(znz_mod_gt) wx' wy) | inr wy' => reduce_n n ((make_op n).(znz_mod_gt) wx wy') end end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1