fact: Definition div_gt x y := match x, y with | N0 wx, N0 wy => let (q, r):= w0_div_gt wx wy in (reduce_0 q, reduce_0 r) | N0 wx, N1 wy => let wx':= GenBase.extend w0_op.(znz_0W) 0 wx in let (q, r):= w1_div_gt wx' wy in (reduce_1 q, reduce_1 r) | N0 wx, N2 wy => let wx':= GenBase.extend w0_op.(znz_0W) 1 wx in let (q, r):= w2_div_gt wx' wy in (reduce_2 q, reduce_2 r) | N0 wx, N3 wy => let wx':= GenBase.extend w0_op.(znz_0W) 2 wx in let (q, r):= w3_div_gt wx' wy in (reduce_3 q, reduce_3 r) | N0 wx, N4 wy => let wx':= GenBase.extend w0_op.(znz_0W) 3 wx in let (q, r):= w4_div_gt wx' wy in (reduce_4 q, reduce_4 r) | N0 wx, N5 wy => let wx':= GenBase.extend w0_op.(znz_0W) 4 wx in let (q, r):= w5_div_gt wx' wy in (reduce_5 q, reduce_5 r) | N0 wx, N6 wy => let wx':= GenBase.extend w0_op.(znz_0W) 5 wx in let (q, r):= w6_div_gt wx' wy in (reduce_6 q, reduce_6 r) | N0 wx, N7 wy => let wx':= GenBase.extend w0_op.(znz_0W) 6 wx in let (q, r):= w7_div_gt wx' wy in (reduce_7 q, reduce_7 r) | N0 wx, N8 wy => let wx':= GenBase.extend w0_op.(znz_0W) 7 wx in let (q, r):= w8_div_gt wx' wy in (reduce_8 q, reduce_8 r) | N0 wx, N9 wy => let wx':= GenBase.extend w0_op.(znz_0W) 8 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N0 wx, N10 wy => let wx':= GenBase.extend w0_op.(znz_0W) 9 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N0 wx, N11 wy => let wx':= GenBase.extend w0_op.(znz_0W) 10 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N0 wx, N12 wy => let wx':= GenBase.extend w0_op.(znz_0W) 11 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N0 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w0_op.(znz_0W) 12 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N1 wx, N0 wy => let (q, r):= w0_divn1 1 wx wy in (reduce_1 q, reduce_0 r) | N1 wx, N1 wy => let (q, r):= w1_div_gt wx wy in (reduce_1 q, reduce_1 r) | N1 wx, N2 wy => let wx':= GenBase.extend w1_op.(znz_0W) 0 wx in let (q, r):= w2_div_gt wx' wy in (reduce_2 q, reduce_2 r) | N1 wx, N3 wy => let wx':= GenBase.extend w1_op.(znz_0W) 1 wx in let (q, r):= w3_div_gt wx' wy in (reduce_3 q, reduce_3 r) | N1 wx, N4 wy => let wx':= GenBase.extend w1_op.(znz_0W) 2 wx in let (q, r):= w4_div_gt wx' wy in (reduce_4 q, reduce_4 r) | N1 wx, N5 wy => let wx':= GenBase.extend w1_op.(znz_0W) 3 wx in let (q, r):= w5_div_gt wx' wy in (reduce_5 q, reduce_5 r) | N1 wx, N6 wy => let wx':= GenBase.extend w1_op.(znz_0W) 4 wx in let (q, r):= w6_div_gt wx' wy in (reduce_6 q, reduce_6 r) | N1 wx, N7 wy => let wx':= GenBase.extend w1_op.(znz_0W) 5 wx in let (q, r):= w7_div_gt wx' wy in (reduce_7 q, reduce_7 r) | N1 wx, N8 wy => let wx':= GenBase.extend w1_op.(znz_0W) 6 wx in let (q, r):= w8_div_gt wx' wy in (reduce_8 q, reduce_8 r) | N1 wx, N9 wy => let wx':= GenBase.extend w1_op.(znz_0W) 7 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N1 wx, N10 wy => let wx':= GenBase.extend w1_op.(znz_0W) 8 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N1 wx, N11 wy => let wx':= GenBase.extend w1_op.(znz_0W) 9 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N1 wx, N12 wy => let wx':= GenBase.extend w1_op.(znz_0W) 10 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N1 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w1_op.(znz_0W) 11 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N2 wx, N0 wy => let (q, r):= w0_divn1 2 wx wy in (reduce_2 q, reduce_0 r) | N2 wx, N1 wy => let (q, r):= w1_divn1 1 wx wy in (reduce_2 q, reduce_1 r) | N2 wx, N2 wy => let (q, r):= w2_div_gt wx wy in (reduce_2 q, reduce_2 r) | N2 wx, N3 wy => let wx':= GenBase.extend w2_op.(znz_0W) 0 wx in let (q, r):= w3_div_gt wx' wy in (reduce_3 q, reduce_3 r) | N2 wx, N4 wy => let wx':= GenBase.extend w2_op.(znz_0W) 1 wx in let (q, r):= w4_div_gt wx' wy in (reduce_4 q, reduce_4 r) | N2 wx, N5 wy => let wx':= GenBase.extend w2_op.(znz_0W) 2 wx in let (q, r):= w5_div_gt wx' wy in (reduce_5 q, reduce_5 r) | N2 wx, N6 wy => let wx':= GenBase.extend w2_op.(znz_0W) 3 wx in let (q, r):= w6_div_gt wx' wy in (reduce_6 q, reduce_6 r) | N2 wx, N7 wy => let wx':= GenBase.extend w2_op.(znz_0W) 4 wx in let (q, r):= w7_div_gt wx' wy in (reduce_7 q, reduce_7 r) | N2 wx, N8 wy => let wx':= GenBase.extend w2_op.(znz_0W) 5 wx in let (q, r):= w8_div_gt wx' wy in (reduce_8 q, reduce_8 r) | N2 wx, N9 wy => let wx':= GenBase.extend w2_op.(znz_0W) 6 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N2 wx, N10 wy => let wx':= GenBase.extend w2_op.(znz_0W) 7 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N2 wx, N11 wy => let wx':= GenBase.extend w2_op.(znz_0W) 8 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N2 wx, N12 wy => let wx':= GenBase.extend w2_op.(znz_0W) 9 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N2 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w2_op.(znz_0W) 10 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N3 wx, N0 wy => let (q, r):= w0_divn1 3 wx wy in (reduce_3 q, reduce_0 r) | N3 wx, N1 wy => let (q, r):= w1_divn1 2 wx wy in (reduce_3 q, reduce_1 r) | N3 wx, N2 wy => let (q, r):= w2_divn1 1 wx wy in (reduce_3 q, reduce_2 r) | N3 wx, N3 wy => let (q, r):= w3_div_gt wx wy in (reduce_3 q, reduce_3 r) | N3 wx, N4 wy => let wx':= GenBase.extend w3_op.(znz_0W) 0 wx in let (q, r):= w4_div_gt wx' wy in (reduce_4 q, reduce_4 r) | N3 wx, N5 wy => let wx':= GenBase.extend w3_op.(znz_0W) 1 wx in let (q, r):= w5_div_gt wx' wy in (reduce_5 q, reduce_5 r) | N3 wx, N6 wy => let wx':= GenBase.extend w3_op.(znz_0W) 2 wx in let (q, r):= w6_div_gt wx' wy in (reduce_6 q, reduce_6 r) | N3 wx, N7 wy => let wx':= GenBase.extend w3_op.(znz_0W) 3 wx in let (q, r):= w7_div_gt wx' wy in (reduce_7 q, reduce_7 r) | N3 wx, N8 wy => let wx':= GenBase.extend w3_op.(znz_0W) 4 wx in let (q, r):= w8_div_gt wx' wy in (reduce_8 q, reduce_8 r) | N3 wx, N9 wy => let wx':= GenBase.extend w3_op.(znz_0W) 5 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N3 wx, N10 wy => let wx':= GenBase.extend w3_op.(znz_0W) 6 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N3 wx, N11 wy => let wx':= GenBase.extend w3_op.(znz_0W) 7 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N3 wx, N12 wy => let wx':= GenBase.extend w3_op.(znz_0W) 8 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N3 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w3_op.(znz_0W) 9 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N4 wx, N0 wy => let (q, r):= w0_divn1 4 wx wy in (reduce_4 q, reduce_0 r) | N4 wx, N1 wy => let (q, r):= w1_divn1 3 wx wy in (reduce_4 q, reduce_1 r) | N4 wx, N2 wy => let (q, r):= w2_divn1 2 wx wy in (reduce_4 q, reduce_2 r) | N4 wx, N3 wy => let (q, r):= w3_divn1 1 wx wy in (reduce_4 q, reduce_3 r) | N4 wx, N4 wy => let (q, r):= w4_div_gt wx wy in (reduce_4 q, reduce_4 r) | N4 wx, N5 wy => let wx':= GenBase.extend w4_op.(znz_0W) 0 wx in let (q, r):= w5_div_gt wx' wy in (reduce_5 q, reduce_5 r) | N4 wx, N6 wy => let wx':= GenBase.extend w4_op.(znz_0W) 1 wx in let (q, r):= w6_div_gt wx' wy in (reduce_6 q, reduce_6 r) | N4 wx, N7 wy => let wx':= GenBase.extend w4_op.(znz_0W) 2 wx in let (q, r):= w7_div_gt wx' wy in (reduce_7 q, reduce_7 r) | N4 wx, N8 wy => let wx':= GenBase.extend w4_op.(znz_0W) 3 wx in let (q, r):= w8_div_gt wx' wy in (reduce_8 q, reduce_8 r) | N4 wx, N9 wy => let wx':= GenBase.extend w4_op.(znz_0W) 4 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N4 wx, N10 wy => let wx':= GenBase.extend w4_op.(znz_0W) 5 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N4 wx, N11 wy => let wx':= GenBase.extend w4_op.(znz_0W) 6 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N4 wx, N12 wy => let wx':= GenBase.extend w4_op.(znz_0W) 7 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N4 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w4_op.(znz_0W) 8 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N5 wx, N0 wy => let (q, r):= w0_divn1 5 wx wy in (reduce_5 q, reduce_0 r) | N5 wx, N1 wy => let (q, r):= w1_divn1 4 wx wy in (reduce_5 q, reduce_1 r) | N5 wx, N2 wy => let (q, r):= w2_divn1 3 wx wy in (reduce_5 q, reduce_2 r) | N5 wx, N3 wy => let (q, r):= w3_divn1 2 wx wy in (reduce_5 q, reduce_3 r) | N5 wx, N4 wy => let (q, r):= w4_divn1 1 wx wy in (reduce_5 q, reduce_4 r) | N5 wx, N5 wy => let (q, r):= w5_div_gt wx wy in (reduce_5 q, reduce_5 r) | N5 wx, N6 wy => let wx':= GenBase.extend w5_op.(znz_0W) 0 wx in let (q, r):= w6_div_gt wx' wy in (reduce_6 q, reduce_6 r) | N5 wx, N7 wy => let wx':= GenBase.extend w5_op.(znz_0W) 1 wx in let (q, r):= w7_div_gt wx' wy in (reduce_7 q, reduce_7 r) | N5 wx, N8 wy => let wx':= GenBase.extend w5_op.(znz_0W) 2 wx in let (q, r):= w8_div_gt wx' wy in (reduce_8 q, reduce_8 r) | N5 wx, N9 wy => let wx':= GenBase.extend w5_op.(znz_0W) 3 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N5 wx, N10 wy => let wx':= GenBase.extend w5_op.(znz_0W) 4 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N5 wx, N11 wy => let wx':= GenBase.extend w5_op.(znz_0W) 5 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N5 wx, N12 wy => let wx':= GenBase.extend w5_op.(znz_0W) 6 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N5 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w5_op.(znz_0W) 7 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N6 wx, N0 wy => let (q, r):= w0_divn1 6 wx wy in (reduce_6 q, reduce_0 r) | N6 wx, N1 wy => let (q, r):= w1_divn1 5 wx wy in (reduce_6 q, reduce_1 r) | N6 wx, N2 wy => let (q, r):= w2_divn1 4 wx wy in (reduce_6 q, reduce_2 r) | N6 wx, N3 wy => let (q, r):= w3_divn1 3 wx wy in (reduce_6 q, reduce_3 r) | N6 wx, N4 wy => let (q, r):= w4_divn1 2 wx wy in (reduce_6 q, reduce_4 r) | N6 wx, N5 wy => let (q, r):= w5_divn1 1 wx wy in (reduce_6 q, reduce_5 r) | N6 wx, N6 wy => let (q, r):= w6_div_gt wx wy in (reduce_6 q, reduce_6 r) | N6 wx, N7 wy => let wx':= GenBase.extend w6_op.(znz_0W) 0 wx in let (q, r):= w7_div_gt wx' wy in (reduce_7 q, reduce_7 r) | N6 wx, N8 wy => let wx':= GenBase.extend w6_op.(znz_0W) 1 wx in let (q, r):= w8_div_gt wx' wy in (reduce_8 q, reduce_8 r) | N6 wx, N9 wy => let wx':= GenBase.extend w6_op.(znz_0W) 2 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N6 wx, N10 wy => let wx':= GenBase.extend w6_op.(znz_0W) 3 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N6 wx, N11 wy => let wx':= GenBase.extend w6_op.(znz_0W) 4 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N6 wx, N12 wy => let wx':= GenBase.extend w6_op.(znz_0W) 5 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N6 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w6_op.(znz_0W) 6 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N7 wx, N0 wy => let (q, r):= w0_divn1 7 wx wy in (reduce_7 q, reduce_0 r) | N7 wx, N1 wy => let (q, r):= w1_divn1 6 wx wy in (reduce_7 q, reduce_1 r) | N7 wx, N2 wy => let (q, r):= w2_divn1 5 wx wy in (reduce_7 q, reduce_2 r) | N7 wx, N3 wy => let (q, r):= w3_divn1 4 wx wy in (reduce_7 q, reduce_3 r) | N7 wx, N4 wy => let (q, r):= w4_divn1 3 wx wy in (reduce_7 q, reduce_4 r) | N7 wx, N5 wy => let (q, r):= w5_divn1 2 wx wy in (reduce_7 q, reduce_5 r) | N7 wx, N6 wy => let (q, r):= w6_divn1 1 wx wy in (reduce_7 q, reduce_6 r) | N7 wx, N7 wy => let (q, r):= w7_div_gt wx wy in (reduce_7 q, reduce_7 r) | N7 wx, N8 wy => let wx':= GenBase.extend w7_op.(znz_0W) 0 wx in let (q, r):= w8_div_gt wx' wy in (reduce_8 q, reduce_8 r) | N7 wx, N9 wy => let wx':= GenBase.extend w7_op.(znz_0W) 1 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N7 wx, N10 wy => let wx':= GenBase.extend w7_op.(znz_0W) 2 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N7 wx, N11 wy => let wx':= GenBase.extend w7_op.(znz_0W) 3 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N7 wx, N12 wy => let wx':= GenBase.extend w7_op.(znz_0W) 4 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N7 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w7_op.(znz_0W) 5 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N8 wx, N0 wy => let (q, r):= w0_divn1 8 wx wy in (reduce_8 q, reduce_0 r) | N8 wx, N1 wy => let (q, r):= w1_divn1 7 wx wy in (reduce_8 q, reduce_1 r) | N8 wx, N2 wy => let (q, r):= w2_divn1 6 wx wy in (reduce_8 q, reduce_2 r) | N8 wx, N3 wy => let (q, r):= w3_divn1 5 wx wy in (reduce_8 q, reduce_3 r) | N8 wx, N4 wy => let (q, r):= w4_divn1 4 wx wy in (reduce_8 q, reduce_4 r) | N8 wx, N5 wy => let (q, r):= w5_divn1 3 wx wy in (reduce_8 q, reduce_5 r) | N8 wx, N6 wy => let (q, r):= w6_divn1 2 wx wy in (reduce_8 q, reduce_6 r) | N8 wx, N7 wy => let (q, r):= w7_divn1 1 wx wy in (reduce_8 q, reduce_7 r) | N8 wx, N8 wy => let (q, r):= w8_div_gt wx wy in (reduce_8 q, reduce_8 r) | N8 wx, N9 wy => let wx':= GenBase.extend w8_op.(znz_0W) 0 wx in let (q, r):= w9_div_gt wx' wy in (reduce_9 q, reduce_9 r) | N8 wx, N10 wy => let wx':= GenBase.extend w8_op.(znz_0W) 1 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N8 wx, N11 wy => let wx':= GenBase.extend w8_op.(znz_0W) 2 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N8 wx, N12 wy => let wx':= GenBase.extend w8_op.(znz_0W) 3 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N8 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w8_op.(znz_0W) 4 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N9 wx, N0 wy => let (q, r):= w0_divn1 9 wx wy in (reduce_9 q, reduce_0 r) | N9 wx, N1 wy => let (q, r):= w1_divn1 8 wx wy in (reduce_9 q, reduce_1 r) | N9 wx, N2 wy => let (q, r):= w2_divn1 7 wx wy in (reduce_9 q, reduce_2 r) | N9 wx, N3 wy => let (q, r):= w3_divn1 6 wx wy in (reduce_9 q, reduce_3 r) | N9 wx, N4 wy => let (q, r):= w4_divn1 5 wx wy in (reduce_9 q, reduce_4 r) | N9 wx, N5 wy => let (q, r):= w5_divn1 4 wx wy in (reduce_9 q, reduce_5 r) | N9 wx, N6 wy => let (q, r):= w6_divn1 3 wx wy in (reduce_9 q, reduce_6 r) | N9 wx, N7 wy => let (q, r):= w7_divn1 2 wx wy in (reduce_9 q, reduce_7 r) | N9 wx, N8 wy => let (q, r):= w8_divn1 1 wx wy in (reduce_9 q, reduce_8 r) | N9 wx, N9 wy => let (q, r):= w9_div_gt wx wy in (reduce_9 q, reduce_9 r) | N9 wx, N10 wy => let wx':= GenBase.extend w9_op.(znz_0W) 0 wx in let (q, r):= w10_div_gt wx' wy in (reduce_10 q, reduce_10 r) | N9 wx, N11 wy => let wx':= GenBase.extend w9_op.(znz_0W) 1 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N9 wx, N12 wy => let wx':= GenBase.extend w9_op.(znz_0W) 2 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N9 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w9_op.(znz_0W) 3 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N10 wx, N0 wy => let (q, r):= w0_divn1 10 wx wy in (reduce_10 q, reduce_0 r) | N10 wx, N1 wy => let (q, r):= w1_divn1 9 wx wy in (reduce_10 q, reduce_1 r) | N10 wx, N2 wy => let (q, r):= w2_divn1 8 wx wy in (reduce_10 q, reduce_2 r) | N10 wx, N3 wy => let (q, r):= w3_divn1 7 wx wy in (reduce_10 q, reduce_3 r) | N10 wx, N4 wy => let (q, r):= w4_divn1 6 wx wy in (reduce_10 q, reduce_4 r) | N10 wx, N5 wy => let (q, r):= w5_divn1 5 wx wy in (reduce_10 q, reduce_5 r) | N10 wx, N6 wy => let (q, r):= w6_divn1 4 wx wy in (reduce_10 q, reduce_6 r) | N10 wx, N7 wy => let (q, r):= w7_divn1 3 wx wy in (reduce_10 q, reduce_7 r) | N10 wx, N8 wy => let (q, r):= w8_divn1 2 wx wy in (reduce_10 q, reduce_8 r) | N10 wx, N9 wy => let (q, r):= w9_divn1 1 wx wy in (reduce_10 q, reduce_9 r) | N10 wx, N10 wy => let (q, r):= w10_div_gt wx wy in (reduce_10 q, reduce_10 r) | N10 wx, N11 wy => let wx':= GenBase.extend w10_op.(znz_0W) 0 wx in let (q, r):= w11_div_gt wx' wy in (reduce_11 q, reduce_11 r) | N10 wx, N12 wy => let wx':= GenBase.extend w10_op.(znz_0W) 1 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N10 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w10_op.(znz_0W) 2 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N11 wx, N0 wy => let (q, r):= w0_divn1 11 wx wy in (reduce_11 q, reduce_0 r) | N11 wx, N1 wy => let (q, r):= w1_divn1 10 wx wy in (reduce_11 q, reduce_1 r) | N11 wx, N2 wy => let (q, r):= w2_divn1 9 wx wy in (reduce_11 q, reduce_2 r) | N11 wx, N3 wy => let (q, r):= w3_divn1 8 wx wy in (reduce_11 q, reduce_3 r) | N11 wx, N4 wy => let (q, r):= w4_divn1 7 wx wy in (reduce_11 q, reduce_4 r) | N11 wx, N5 wy => let (q, r):= w5_divn1 6 wx wy in (reduce_11 q, reduce_5 r) | N11 wx, N6 wy => let (q, r):= w6_divn1 5 wx wy in (reduce_11 q, reduce_6 r) | N11 wx, N7 wy => let (q, r):= w7_divn1 4 wx wy in (reduce_11 q, reduce_7 r) | N11 wx, N8 wy => let (q, r):= w8_divn1 3 wx wy in (reduce_11 q, reduce_8 r) | N11 wx, N9 wy => let (q, r):= w9_divn1 2 wx wy in (reduce_11 q, reduce_9 r) | N11 wx, N10 wy => let (q, r):= w10_divn1 1 wx wy in (reduce_11 q, reduce_10 r) | N11 wx, N11 wy => let (q, r):= w11_div_gt wx wy in (reduce_11 q, reduce_11 r) | N11 wx, N12 wy => let wx':= GenBase.extend w11_op.(znz_0W) 0 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) | N11 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w11_op.(znz_0W) 1 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N12 wx, N0 wy => let (q, r):= w0_divn1 12 wx wy in (reduce_12 q, reduce_0 r) | N12 wx, N1 wy => let (q, r):= w1_divn1 11 wx wy in (reduce_12 q, reduce_1 r) | N12 wx, N2 wy => let (q, r):= w2_divn1 10 wx wy in (reduce_12 q, reduce_2 r) | N12 wx, N3 wy => let (q, r):= w3_divn1 9 wx wy in (reduce_12 q, reduce_3 r) | N12 wx, N4 wy => let (q, r):= w4_divn1 8 wx wy in (reduce_12 q, reduce_4 r) | N12 wx, N5 wy => let (q, r):= w5_divn1 7 wx wy in (reduce_12 q, reduce_5 r) | N12 wx, N6 wy => let (q, r):= w6_divn1 6 wx wy in (reduce_12 q, reduce_6 r) | N12 wx, N7 wy => let (q, r):= w7_divn1 5 wx wy in (reduce_12 q, reduce_7 r) | N12 wx, N8 wy => let (q, r):= w8_divn1 4 wx wy in (reduce_12 q, reduce_8 r) | N12 wx, N9 wy => let (q, r):= w9_divn1 3 wx wy in (reduce_12 q, reduce_9 r) | N12 wx, N10 wy => let (q, r):= w10_divn1 2 wx wy in (reduce_12 q, reduce_10 r) | N12 wx, N11 wy => let (q, r):= w11_divn1 1 wx wy in (reduce_12 q, reduce_11 r) | N12 wx, N12 wy => let (q, r):= w12_div_gt wx wy in (reduce_12 q, reduce_12 r) | N12 wx, Nn n wy => let wx':= extend n w12 (GenBase.extend w12_op.(znz_0W) 0 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | Nn n wx, N0 wy => let wy':= GenBase.extend w0_op.(znz_0W) 11 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N1 wy => let wy':= GenBase.extend w1_op.(znz_0W) 10 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N2 wy => let wy':= GenBase.extend w2_op.(znz_0W) 9 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N3 wy => let wy':= GenBase.extend w3_op.(znz_0W) 8 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N4 wy => let wy':= GenBase.extend w4_op.(znz_0W) 7 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N5 wy => let wy':= GenBase.extend w5_op.(znz_0W) 6 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N6 wy => let wy':= GenBase.extend w6_op.(znz_0W) 5 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N7 wy => let wy':= GenBase.extend w7_op.(znz_0W) 4 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N8 wy => let wy':= GenBase.extend w8_op.(znz_0W) 3 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N9 wy => let wy':= GenBase.extend w9_op.(znz_0W) 2 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N10 wy => let wy':= GenBase.extend w10_op.(znz_0W) 1 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N11 wy => let wy':= GenBase.extend w11_op.(znz_0W) 0 wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, N12 wy => let wy':= wy in let (q, r):= w12_divn1 (S n) wx wy' in (reduce_n n q, reduce_12 r) | Nn n wx, Nn m wy => match extend_to_max w12 n m wx wy with | inl wx' => let (q, r):= (make_op m).(znz_div) wx' wy in (reduce_n m q, reduce_n m r) | inr wy' => let (q, r):= (make_op n).(znz_div) wx wy' in (reduce_n n q, reduce_n n r) end end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1