fact: Definition addn n (x y : word w12 (S n)) := let op := make_op n in match op.(znz_add_c) x y with | C0 r => Nn n r | C1 r => Nn (S n) (WW op.(znz_1) r) end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1