fact: Definition compare x y := match x, y with | N0 wx, N0 wy => compare_0 wx wy | N0 wx, N1 wy => opp_compare (comparen_0 1 wy wx) | N0 wx, N2 wy => opp_compare (comparen_0 2 wy wx) | N0 wx, N3 wy => opp_compare (comparen_0 3 wy wx) | N0 wx, N4 wy => opp_compare (comparen_0 4 wy wx) | N0 wx, N5 wy => opp_compare (comparen_0 5 wy wx) | N0 wx, N6 wy => opp_compare (comparen_0 6 wy wx) | N0 wx, N7 wy => opp_compare (comparen_0 7 wy wx) | N0 wx, N8 wy => opp_compare (comparen_0 8 wy wx) | N0 wx, N9 wy => opp_compare (comparen_0 9 wy wx) | N0 wx, N10 wy => opp_compare (comparen_0 10 wy wx) | N0 wx, N11 wy => opp_compare (comparen_0 11 wy wx) | N0 wx, N12 wy => opp_compare (comparen_0 12 wy wx) | N0 wx, Nn n wy => opp_compare (compare_mn_1 w12 w0 w_0 compare_0 (compare_12 W0) (comparen_0 12) (S n) wy wx) | N1 wx, N0 wy => comparen_0 1 wx wy | N1 wx, N1 wy => compare_1 wx wy | N1 wx, N2 wy => opp_compare (comparen_1 1 wy wx) | N1 wx, N3 wy => opp_compare (comparen_1 2 wy wx) | N1 wx, N4 wy => opp_compare (comparen_1 3 wy wx) | N1 wx, N5 wy => opp_compare (comparen_1 4 wy wx) | N1 wx, N6 wy => opp_compare (comparen_1 5 wy wx) | N1 wx, N7 wy => opp_compare (comparen_1 6 wy wx) | N1 wx, N8 wy => opp_compare (comparen_1 7 wy wx) | N1 wx, N9 wy => opp_compare (comparen_1 8 wy wx) | N1 wx, N10 wy => opp_compare (comparen_1 9 wy wx) | N1 wx, N11 wy => opp_compare (comparen_1 10 wy wx) | N1 wx, N12 wy => opp_compare (comparen_1 11 wy wx) | N1 wx, Nn n wy => opp_compare (compare_mn_1 w12 w1 W0 compare_1 (compare_12 W0) (comparen_1 11) (S n) wy wx) | N2 wx, N0 wy => comparen_0 2 wx wy | N2 wx, N1 wy => comparen_1 1 wx wy | N2 wx, N2 wy => compare_2 wx wy | N2 wx, N3 wy => opp_compare (comparen_2 1 wy wx) | N2 wx, N4 wy => opp_compare (comparen_2 2 wy wx) | N2 wx, N5 wy => opp_compare (comparen_2 3 wy wx) | N2 wx, N6 wy => opp_compare (comparen_2 4 wy wx) | N2 wx, N7 wy => opp_compare (comparen_2 5 wy wx) | N2 wx, N8 wy => opp_compare (comparen_2 6 wy wx) | N2 wx, N9 wy => opp_compare (comparen_2 7 wy wx) | N2 wx, N10 wy => opp_compare (comparen_2 8 wy wx) | N2 wx, N11 wy => opp_compare (comparen_2 9 wy wx) | N2 wx, N12 wy => opp_compare (comparen_2 10 wy wx) | N2 wx, Nn n wy => opp_compare (compare_mn_1 w12 w2 W0 compare_2 (compare_12 W0) (comparen_2 10) (S n) wy wx) | N3 wx, N0 wy => comparen_0 3 wx wy | N3 wx, N1 wy => comparen_1 2 wx wy | N3 wx, N2 wy => comparen_2 1 wx wy | N3 wx, N3 wy => compare_3 wx wy | N3 wx, N4 wy => opp_compare (comparen_3 1 wy wx) | N3 wx, N5 wy => opp_compare (comparen_3 2 wy wx) | N3 wx, N6 wy => opp_compare (comparen_3 3 wy wx) | N3 wx, N7 wy => opp_compare (comparen_3 4 wy wx) | N3 wx, N8 wy => opp_compare (comparen_3 5 wy wx) | N3 wx, N9 wy => opp_compare (comparen_3 6 wy wx) | N3 wx, N10 wy => opp_compare (comparen_3 7 wy wx) | N3 wx, N11 wy => opp_compare (comparen_3 8 wy wx) | N3 wx, N12 wy => opp_compare (comparen_3 9 wy wx) | N3 wx, Nn n wy => opp_compare (compare_mn_1 w12 w3 W0 compare_3 (compare_12 W0) (comparen_3 9) (S n) wy wx) | N4 wx, N0 wy => comparen_0 4 wx wy | N4 wx, N1 wy => comparen_1 3 wx wy | N4 wx, N2 wy => comparen_2 2 wx wy | N4 wx, N3 wy => comparen_3 1 wx wy | N4 wx, N4 wy => compare_4 wx wy | N4 wx, N5 wy => opp_compare (comparen_4 1 wy wx) | N4 wx, N6 wy => opp_compare (comparen_4 2 wy wx) | N4 wx, N7 wy => opp_compare (comparen_4 3 wy wx) | N4 wx, N8 wy => opp_compare (comparen_4 4 wy wx) | N4 wx, N9 wy => opp_compare (comparen_4 5 wy wx) | N4 wx, N10 wy => opp_compare (comparen_4 6 wy wx) | N4 wx, N11 wy => opp_compare (comparen_4 7 wy wx) | N4 wx, N12 wy => opp_compare (comparen_4 8 wy wx) | N4 wx, Nn n wy => opp_compare (compare_mn_1 w12 w4 W0 compare_4 (compare_12 W0) (comparen_4 8) (S n) wy wx) | N5 wx, N0 wy => comparen_0 5 wx wy | N5 wx, N1 wy => comparen_1 4 wx wy | N5 wx, N2 wy => comparen_2 3 wx wy | N5 wx, N3 wy => comparen_3 2 wx wy | N5 wx, N4 wy => comparen_4 1 wx wy | N5 wx, N5 wy => compare_5 wx wy | N5 wx, N6 wy => opp_compare (comparen_5 1 wy wx) | N5 wx, N7 wy => opp_compare (comparen_5 2 wy wx) | N5 wx, N8 wy => opp_compare (comparen_5 3 wy wx) | N5 wx, N9 wy => opp_compare (comparen_5 4 wy wx) | N5 wx, N10 wy => opp_compare (comparen_5 5 wy wx) | N5 wx, N11 wy => opp_compare (comparen_5 6 wy wx) | N5 wx, N12 wy => opp_compare (comparen_5 7 wy wx) | N5 wx, Nn n wy => opp_compare (compare_mn_1 w12 w5 W0 compare_5 (compare_12 W0) (comparen_5 7) (S n) wy wx) | N6 wx, N0 wy => comparen_0 6 wx wy | N6 wx, N1 wy => comparen_1 5 wx wy | N6 wx, N2 wy => comparen_2 4 wx wy | N6 wx, N3 wy => comparen_3 3 wx wy | N6 wx, N4 wy => comparen_4 2 wx wy | N6 wx, N5 wy => comparen_5 1 wx wy | N6 wx, N6 wy => compare_6 wx wy | N6 wx, N7 wy => opp_compare (comparen_6 1 wy wx) | N6 wx, N8 wy => opp_compare (comparen_6 2 wy wx) | N6 wx, N9 wy => opp_compare (comparen_6 3 wy wx) | N6 wx, N10 wy => opp_compare (comparen_6 4 wy wx) | N6 wx, N11 wy => opp_compare (comparen_6 5 wy wx) | N6 wx, N12 wy => opp_compare (comparen_6 6 wy wx) | N6 wx, Nn n wy => opp_compare (compare_mn_1 w12 w6 W0 compare_6 (compare_12 W0) (comparen_6 6) (S n) wy wx) | N7 wx, N0 wy => comparen_0 7 wx wy | N7 wx, N1 wy => comparen_1 6 wx wy | N7 wx, N2 wy => comparen_2 5 wx wy | N7 wx, N3 wy => comparen_3 4 wx wy | N7 wx, N4 wy => comparen_4 3 wx wy | N7 wx, N5 wy => comparen_5 2 wx wy | N7 wx, N6 wy => comparen_6 1 wx wy | N7 wx, N7 wy => compare_7 wx wy | N7 wx, N8 wy => opp_compare (comparen_7 1 wy wx) | N7 wx, N9 wy => opp_compare (comparen_7 2 wy wx) | N7 wx, N10 wy => opp_compare (comparen_7 3 wy wx) | N7 wx, N11 wy => opp_compare (comparen_7 4 wy wx) | N7 wx, N12 wy => opp_compare (comparen_7 5 wy wx) | N7 wx, Nn n wy => opp_compare (compare_mn_1 w12 w7 W0 compare_7 (compare_12 W0) (comparen_7 5) (S n) wy wx) | N8 wx, N0 wy => comparen_0 8 wx wy | N8 wx, N1 wy => comparen_1 7 wx wy | N8 wx, N2 wy => comparen_2 6 wx wy | N8 wx, N3 wy => comparen_3 5 wx wy | N8 wx, N4 wy => comparen_4 4 wx wy | N8 wx, N5 wy => comparen_5 3 wx wy | N8 wx, N6 wy => comparen_6 2 wx wy | N8 wx, N7 wy => comparen_7 1 wx wy | N8 wx, N8 wy => compare_8 wx wy | N8 wx, N9 wy => opp_compare (comparen_8 1 wy wx) | N8 wx, N10 wy => opp_compare (comparen_8 2 wy wx) | N8 wx, N11 wy => opp_compare (comparen_8 3 wy wx) | N8 wx, N12 wy => opp_compare (comparen_8 4 wy wx) | N8 wx, Nn n wy => opp_compare (compare_mn_1 w12 w8 W0 compare_8 (compare_12 W0) (comparen_8 4) (S n) wy wx) | N9 wx, N0 wy => comparen_0 9 wx wy | N9 wx, N1 wy => comparen_1 8 wx wy | N9 wx, N2 wy => comparen_2 7 wx wy | N9 wx, N3 wy => comparen_3 6 wx wy | N9 wx, N4 wy => comparen_4 5 wx wy | N9 wx, N5 wy => comparen_5 4 wx wy | N9 wx, N6 wy => comparen_6 3 wx wy | N9 wx, N7 wy => comparen_7 2 wx wy | N9 wx, N8 wy => comparen_8 1 wx wy | N9 wx, N9 wy => compare_9 wx wy | N9 wx, N10 wy => opp_compare (comparen_9 1 wy wx) | N9 wx, N11 wy => opp_compare (comparen_9 2 wy wx) | N9 wx, N12 wy => opp_compare (comparen_9 3 wy wx) | N9 wx, Nn n wy => opp_compare (compare_mn_1 w12 w9 W0 compare_9 (compare_12 W0) (comparen_9 3) (S n) wy wx) | N10 wx, N0 wy => comparen_0 10 wx wy | N10 wx, N1 wy => comparen_1 9 wx wy | N10 wx, N2 wy => comparen_2 8 wx wy | N10 wx, N3 wy => comparen_3 7 wx wy | N10 wx, N4 wy => comparen_4 6 wx wy | N10 wx, N5 wy => comparen_5 5 wx wy | N10 wx, N6 wy => comparen_6 4 wx wy | N10 wx, N7 wy => comparen_7 3 wx wy | N10 wx, N8 wy => comparen_8 2 wx wy | N10 wx, N9 wy => comparen_9 1 wx wy | N10 wx, N10 wy => compare_10 wx wy | N10 wx, N11 wy => opp_compare (comparen_10 1 wy wx) | N10 wx, N12 wy => opp_compare (comparen_10 2 wy wx) | N10 wx, Nn n wy => opp_compare (compare_mn_1 w12 w10 W0 compare_10 (compare_12 W0) (comparen_10 2) (S n) wy wx) | N11 wx, N0 wy => comparen_0 11 wx wy | N11 wx, N1 wy => comparen_1 10 wx wy | N11 wx, N2 wy => comparen_2 9 wx wy | N11 wx, N3 wy => comparen_3 8 wx wy | N11 wx, N4 wy => comparen_4 7 wx wy | N11 wx, N5 wy => comparen_5 6 wx wy | N11 wx, N6 wy => comparen_6 5 wx wy | N11 wx, N7 wy => comparen_7 4 wx wy | N11 wx, N8 wy => comparen_8 3 wx wy | N11 wx, N9 wy => comparen_9 2 wx wy | N11 wx, N10 wy => comparen_10 1 wx wy | N11 wx, N11 wy => compare_11 wx wy | N11 wx, N12 wy => opp_compare (comparen_11 1 wy wx) | N11 wx, Nn n wy => opp_compare (compare_mn_1 w12 w11 W0 compare_11 (compare_12 W0) (comparen_11 1) (S n) wy wx) | N12 wx, N0 wy => comparen_0 12 wx wy | N12 wx, N1 wy => comparen_1 11 wx wy | N12 wx, N2 wy => comparen_2 10 wx wy | N12 wx, N3 wy => comparen_3 9 wx wy | N12 wx, N4 wy => comparen_4 8 wx wy | N12 wx, N5 wy => comparen_5 7 wx wy | N12 wx, N6 wy => comparen_6 6 wx wy | N12 wx, N7 wy => comparen_7 5 wx wy | N12 wx, N8 wy => comparen_8 4 wx wy | N12 wx, N9 wy => comparen_9 3 wx wy | N12 wx, N10 wy => comparen_10 2 wx wy | N12 wx, N11 wy => comparen_11 1 wx wy | N12 wx, N12 wy => compare_12 wx wy | N12 wx, Nn n wy => opp_compare (compare_mn_1 w12 w12 W0 compare_12 (compare_12 W0) (comparen_12 0) (S n) wy wx) | Nn n wx, N0 wy => compare_mn_1 w12 w0 w_0 compare_0 (compare_12 W0) (comparen_0 12) (S n) wx wy | Nn n wx, N1 wy => compare_mn_1 w12 w1 W0 compare_1 (compare_12 W0) (comparen_1 11) (S n) wx wy | Nn n wx, N2 wy => compare_mn_1 w12 w2 W0 compare_2 (compare_12 W0) (comparen_2 10) (S n) wx wy | Nn n wx, N3 wy => compare_mn_1 w12 w3 W0 compare_3 (compare_12 W0) (comparen_3 9) (S n) wx wy | Nn n wx, N4 wy => compare_mn_1 w12 w4 W0 compare_4 (compare_12 W0) (comparen_4 8) (S n) wx wy | Nn n wx, N5 wy => compare_mn_1 w12 w5 W0 compare_5 (compare_12 W0) (comparen_5 7) (S n) wx wy | Nn n wx, N6 wy => compare_mn_1 w12 w6 W0 compare_6 (compare_12 W0) (comparen_6 6) (S n) wx wy | Nn n wx, N7 wy => compare_mn_1 w12 w7 W0 compare_7 (compare_12 W0) (comparen_7 5) (S n) wx wy | Nn n wx, N8 wy => compare_mn_1 w12 w8 W0 compare_8 (compare_12 W0) (comparen_8 4) (S n) wx wy | Nn n wx, N9 wy => compare_mn_1 w12 w9 W0 compare_9 (compare_12 W0) (comparen_9 3) (S n) wx wy | Nn n wx, N10 wy => compare_mn_1 w12 w10 W0 compare_10 (compare_12 W0) (comparen_10 2) (S n) wx wy | Nn n wx, N11 wy => compare_mn_1 w12 w11 W0 compare_11 (compare_12 W0) (comparen_11 1) (S n) wx wy | Nn n wx, N12 wy => compare_mn_1 w12 w12 W0 compare_12 (compare_12 W0) (comparen_12 0) (S n) wx wy | Nn n wx, Nn m wy => match extend_to_max w12 n m wx wy with | inl wx' => let op := make_op m in op.(znz_compare) wx' wy | inr wy' => let op := make_op n in op.(znz_compare) wx wy' end end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1