fact: Definition add x y := match x, y with | N0 wx, N0 wy => w0_add wx wy | N0 wx, N1 wy => if w0_eq0 wx then y else w1_add (WW w_0 wx) wy | N0 wx, N2 wy => if w0_eq0 wx then y else w2_add (extend1 w0 (WW w_0 wx)) wy | N0 wx, N3 wy => if w0_eq0 wx then y else w3_add (extend2 w0 (WW w_0 wx)) wy | N0 wx, N4 wy => if w0_eq0 wx then y else w4_add (extend3 w0 (WW w_0 wx)) wy | N0 wx, N5 wy => if w0_eq0 wx then y else w5_add (extend4 w0 (WW w_0 wx)) wy | N0 wx, N6 wy => if w0_eq0 wx then y else w6_add (extend5 w0 (WW w_0 wx)) wy | N0 wx, N7 wy => if w0_eq0 wx then y else w7_add (extend6 w0 (WW w_0 wx)) wy | N0 wx, N8 wy => if w0_eq0 wx then y else w8_add (extend7 w0 (WW w_0 wx)) wy | N0 wx, N9 wy => if w0_eq0 wx then y else w9_add (extend8 w0 (WW w_0 wx)) wy | N0 wx, N10 wy => if w0_eq0 wx then y else w10_add (extend9 w0 (WW w_0 wx)) wy | N0 wx, N11 wy => if w0_eq0 wx then y else w11_add (extend10 w0 (WW w_0 wx)) wy | N0 wx, N12 wy => if w0_eq0 wx then y else w12_add (extend11 w0 (WW w_0 wx)) wy | N0 wx, Nn n wy => if w0_eq0 wx then y else addn n (extend n w12 (extend12 w0 (WW w_0 wx))) wy | N1 wx, N0 wy => if w0_eq0 wy then x else w1_add wx (WW w_0 wy) | N1 wx, N1 wy => w1_add wx wy | N1 wx, N2 wy => w2_add (extend1 w0 wx) wy | N1 wx, N3 wy => w3_add (extend2 w0 wx) wy | N1 wx, N4 wy => w4_add (extend3 w0 wx) wy | N1 wx, N5 wy => w5_add (extend4 w0 wx) wy | N1 wx, N6 wy => w6_add (extend5 w0 wx) wy | N1 wx, N7 wy => w7_add (extend6 w0 wx) wy | N1 wx, N8 wy => w8_add (extend7 w0 wx) wy | N1 wx, N9 wy => w9_add (extend8 w0 wx) wy | N1 wx, N10 wy => w10_add (extend9 w0 wx) wy | N1 wx, N11 wy => w11_add (extend10 w0 wx) wy | N1 wx, N12 wy => w12_add (extend11 w0 wx) wy | N1 wx, Nn n wy => addn n (extend n w12 (extend12 w0 wx)) wy | N2 wx, N0 wy => if w0_eq0 wy then x else w2_add wx (extend1 w0 (WW w_0 wy)) | N2 wx, N1 wy => w2_add wx (extend1 w0 wy) | N2 wx, N2 wy => w2_add wx wy | N2 wx, N3 wy => w3_add (extend1 w1 wx) wy | N2 wx, N4 wy => w4_add (extend2 w1 wx) wy | N2 wx, N5 wy => w5_add (extend3 w1 wx) wy | N2 wx, N6 wy => w6_add (extend4 w1 wx) wy | N2 wx, N7 wy => w7_add (extend5 w1 wx) wy | N2 wx, N8 wy => w8_add (extend6 w1 wx) wy | N2 wx, N9 wy => w9_add (extend7 w1 wx) wy | N2 wx, N10 wy => w10_add (extend8 w1 wx) wy | N2 wx, N11 wy => w11_add (extend9 w1 wx) wy | N2 wx, N12 wy => w12_add (extend10 w1 wx) wy | N2 wx, Nn n wy => addn n (extend n w12 (extend11 w1 wx)) wy | N3 wx, N0 wy => if w0_eq0 wy then x else w3_add wx (extend2 w0 (WW w_0 wy)) | N3 wx, N1 wy => w3_add wx (extend2 w0 wy) | N3 wx, N2 wy => w3_add wx (extend1 w1 wy) | N3 wx, N3 wy => w3_add wx wy | N3 wx, N4 wy => w4_add (extend1 w2 wx) wy | N3 wx, N5 wy => w5_add (extend2 w2 wx) wy | N3 wx, N6 wy => w6_add (extend3 w2 wx) wy | N3 wx, N7 wy => w7_add (extend4 w2 wx) wy | N3 wx, N8 wy => w8_add (extend5 w2 wx) wy | N3 wx, N9 wy => w9_add (extend6 w2 wx) wy | N3 wx, N10 wy => w10_add (extend7 w2 wx) wy | N3 wx, N11 wy => w11_add (extend8 w2 wx) wy | N3 wx, N12 wy => w12_add (extend9 w2 wx) wy | N3 wx, Nn n wy => addn n (extend n w12 (extend10 w2 wx)) wy | N4 wx, N0 wy => if w0_eq0 wy then x else w4_add wx (extend3 w0 (WW w_0 wy)) | N4 wx, N1 wy => w4_add wx (extend3 w0 wy) | N4 wx, N2 wy => w4_add wx (extend2 w1 wy) | N4 wx, N3 wy => w4_add wx (extend1 w2 wy) | N4 wx, N4 wy => w4_add wx wy | N4 wx, N5 wy => w5_add (extend1 w3 wx) wy | N4 wx, N6 wy => w6_add (extend2 w3 wx) wy | N4 wx, N7 wy => w7_add (extend3 w3 wx) wy | N4 wx, N8 wy => w8_add (extend4 w3 wx) wy | N4 wx, N9 wy => w9_add (extend5 w3 wx) wy | N4 wx, N10 wy => w10_add (extend6 w3 wx) wy | N4 wx, N11 wy => w11_add (extend7 w3 wx) wy | N4 wx, N12 wy => w12_add (extend8 w3 wx) wy | N4 wx, Nn n wy => addn n (extend n w12 (extend9 w3 wx)) wy | N5 wx, N0 wy => if w0_eq0 wy then x else w5_add wx (extend4 w0 (WW w_0 wy)) | N5 wx, N1 wy => w5_add wx (extend4 w0 wy) | N5 wx, N2 wy => w5_add wx (extend3 w1 wy) | N5 wx, N3 wy => w5_add wx (extend2 w2 wy) | N5 wx, N4 wy => w5_add wx (extend1 w3 wy) | N5 wx, N5 wy => w5_add wx wy | N5 wx, N6 wy => w6_add (extend1 w4 wx) wy | N5 wx, N7 wy => w7_add (extend2 w4 wx) wy | N5 wx, N8 wy => w8_add (extend3 w4 wx) wy | N5 wx, N9 wy => w9_add (extend4 w4 wx) wy | N5 wx, N10 wy => w10_add (extend5 w4 wx) wy | N5 wx, N11 wy => w11_add (extend6 w4 wx) wy | N5 wx, N12 wy => w12_add (extend7 w4 wx) wy | N5 wx, Nn n wy => addn n (extend n w12 (extend8 w4 wx)) wy | N6 wx, N0 wy => if w0_eq0 wy then x else w6_add wx (extend5 w0 (WW w_0 wy)) | N6 wx, N1 wy => w6_add wx (extend5 w0 wy) | N6 wx, N2 wy => w6_add wx (extend4 w1 wy) | N6 wx, N3 wy => w6_add wx (extend3 w2 wy) | N6 wx, N4 wy => w6_add wx (extend2 w3 wy) | N6 wx, N5 wy => w6_add wx (extend1 w4 wy) | N6 wx, N6 wy => w6_add wx wy | N6 wx, N7 wy => w7_add (extend1 w5 wx) wy | N6 wx, N8 wy => w8_add (extend2 w5 wx) wy | N6 wx, N9 wy => w9_add (extend3 w5 wx) wy | N6 wx, N10 wy => w10_add (extend4 w5 wx) wy | N6 wx, N11 wy => w11_add (extend5 w5 wx) wy | N6 wx, N12 wy => w12_add (extend6 w5 wx) wy | N6 wx, Nn n wy => addn n (extend n w12 (extend7 w5 wx)) wy | N7 wx, N0 wy => if w0_eq0 wy then x else w7_add wx (extend6 w0 (WW w_0 wy)) | N7 wx, N1 wy => w7_add wx (extend6 w0 wy) | N7 wx, N2 wy => w7_add wx (extend5 w1 wy) | N7 wx, N3 wy => w7_add wx (extend4 w2 wy) | N7 wx, N4 wy => w7_add wx (extend3 w3 wy) | N7 wx, N5 wy => w7_add wx (extend2 w4 wy) | N7 wx, N6 wy => w7_add wx (extend1 w5 wy) | N7 wx, N7 wy => w7_add wx wy | N7 wx, N8 wy => w8_add (extend1 w6 wx) wy | N7 wx, N9 wy => w9_add (extend2 w6 wx) wy | N7 wx, N10 wy => w10_add (extend3 w6 wx) wy | N7 wx, N11 wy => w11_add (extend4 w6 wx) wy | N7 wx, N12 wy => w12_add (extend5 w6 wx) wy | N7 wx, Nn n wy => addn n (extend n w12 (extend6 w6 wx)) wy | N8 wx, N0 wy => if w0_eq0 wy then x else w8_add wx (extend7 w0 (WW w_0 wy)) | N8 wx, N1 wy => w8_add wx (extend7 w0 wy) | N8 wx, N2 wy => w8_add wx (extend6 w1 wy) | N8 wx, N3 wy => w8_add wx (extend5 w2 wy) | N8 wx, N4 wy => w8_add wx (extend4 w3 wy) | N8 wx, N5 wy => w8_add wx (extend3 w4 wy) | N8 wx, N6 wy => w8_add wx (extend2 w5 wy) | N8 wx, N7 wy => w8_add wx (extend1 w6 wy) | N8 wx, N8 wy => w8_add wx wy | N8 wx, N9 wy => w9_add (extend1 w7 wx) wy | N8 wx, N10 wy => w10_add (extend2 w7 wx) wy | N8 wx, N11 wy => w11_add (extend3 w7 wx) wy | N8 wx, N12 wy => w12_add (extend4 w7 wx) wy | N8 wx, Nn n wy => addn n (extend n w12 (extend5 w7 wx)) wy | N9 wx, N0 wy => if w0_eq0 wy then x else w9_add wx (extend8 w0 (WW w_0 wy)) | N9 wx, N1 wy => w9_add wx (extend8 w0 wy) | N9 wx, N2 wy => w9_add wx (extend7 w1 wy) | N9 wx, N3 wy => w9_add wx (extend6 w2 wy) | N9 wx, N4 wy => w9_add wx (extend5 w3 wy) | N9 wx, N5 wy => w9_add wx (extend4 w4 wy) | N9 wx, N6 wy => w9_add wx (extend3 w5 wy) | N9 wx, N7 wy => w9_add wx (extend2 w6 wy) | N9 wx, N8 wy => w9_add wx (extend1 w7 wy) | N9 wx, N9 wy => w9_add wx wy | N9 wx, N10 wy => w10_add (extend1 w8 wx) wy | N9 wx, N11 wy => w11_add (extend2 w8 wx) wy | N9 wx, N12 wy => w12_add (extend3 w8 wx) wy | N9 wx, Nn n wy => addn n (extend n w12 (extend4 w8 wx)) wy | N10 wx, N0 wy => if w0_eq0 wy then x else w10_add wx (extend9 w0 (WW w_0 wy)) | N10 wx, N1 wy => w10_add wx (extend9 w0 wy) | N10 wx, N2 wy => w10_add wx (extend8 w1 wy) | N10 wx, N3 wy => w10_add wx (extend7 w2 wy) | N10 wx, N4 wy => w10_add wx (extend6 w3 wy) | N10 wx, N5 wy => w10_add wx (extend5 w4 wy) | N10 wx, N6 wy => w10_add wx (extend4 w5 wy) | N10 wx, N7 wy => w10_add wx (extend3 w6 wy) | N10 wx, N8 wy => w10_add wx (extend2 w7 wy) | N10 wx, N9 wy => w10_add wx (extend1 w8 wy) | N10 wx, N10 wy => w10_add wx wy | N10 wx, N11 wy => w11_add (extend1 w9 wx) wy | N10 wx, N12 wy => w12_add (extend2 w9 wx) wy | N10 wx, Nn n wy => addn n (extend n w12 (extend3 w9 wx)) wy | N11 wx, N0 wy => if w0_eq0 wy then x else w11_add wx (extend10 w0 (WW w_0 wy)) | N11 wx, N1 wy => w11_add wx (extend10 w0 wy) | N11 wx, N2 wy => w11_add wx (extend9 w1 wy) | N11 wx, N3 wy => w11_add wx (extend8 w2 wy) | N11 wx, N4 wy => w11_add wx (extend7 w3 wy) | N11 wx, N5 wy => w11_add wx (extend6 w4 wy) | N11 wx, N6 wy => w11_add wx (extend5 w5 wy) | N11 wx, N7 wy => w11_add wx (extend4 w6 wy) | N11 wx, N8 wy => w11_add wx (extend3 w7 wy) | N11 wx, N9 wy => w11_add wx (extend2 w8 wy) | N11 wx, N10 wy => w11_add wx (extend1 w9 wy) | N11 wx, N11 wy => w11_add wx wy | N11 wx, N12 wy => w12_add (extend1 w10 wx) wy | N11 wx, Nn n wy => addn n (extend n w12 (extend2 w10 wx)) wy | N12 wx, N0 wy => if w0_eq0 wy then x else w12_add wx (extend11 w0 (WW w_0 wy)) | N12 wx, N1 wy => w12_add wx (extend11 w0 wy) | N12 wx, N2 wy => w12_add wx (extend10 w1 wy) | N12 wx, N3 wy => w12_add wx (extend9 w2 wy) | N12 wx, N4 wy => w12_add wx (extend8 w3 wy) | N12 wx, N5 wy => w12_add wx (extend7 w4 wy) | N12 wx, N6 wy => w12_add wx (extend6 w5 wy) | N12 wx, N7 wy => w12_add wx (extend5 w6 wy) | N12 wx, N8 wy => w12_add wx (extend4 w7 wy) | N12 wx, N9 wy => w12_add wx (extend3 w8 wy) | N12 wx, N10 wy => w12_add wx (extend2 w9 wy) | N12 wx, N11 wy => w12_add wx (extend1 w10 wy) | N12 wx, N12 wy => w12_add wx wy | N12 wx, Nn n wy => addn n (extend n w12 (extend1 w11 wx)) wy | Nn n wx, N0 wy => if w0_eq0 wy then x else addn n wx (extend n w12 (extend12 w0 (WW w_0 wy))) | Nn n wx, N1 wy => addn n wx (extend n w12 (extend12 w0 wy)) | Nn n wx, N2 wy => addn n wx (extend n w12 (extend11 w1 wy)) | Nn n wx, N3 wy => addn n wx (extend n w12 (extend10 w2 wy)) | Nn n wx, N4 wy => addn n wx (extend n w12 (extend9 w3 wy)) | Nn n wx, N5 wy => addn n wx (extend n w12 (extend8 w4 wy)) | Nn n wx, N6 wy => addn n wx (extend n w12 (extend7 w5 wy)) | Nn n wx, N7 wy => addn n wx (extend n w12 (extend6 w6 wy)) | Nn n wx, N8 wy => addn n wx (extend n w12 (extend5 w7 wy)) | Nn n wx, N9 wy => addn n wx (extend n w12 (extend4 w8 wy)) | Nn n wx, N10 wy => addn n wx (extend n w12 (extend3 w9 wy)) | Nn n wx, N11 wy => addn n wx (extend n w12 (extend2 w10 wy)) | Nn n wx, N12 wy => addn n wx (extend n w12 (extend1 w11 wy)) | Nn n wx, Nn m wy => match extend_to_max w12 n m wx wy with | inl wx' => addn m wx' wy | inr wy' => addn n wx wy' end end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1