fact: Fixpoint make_op_aux (n:nat) : znz_op (word w12 (S n)):= match n return znz_op (word w12 (S n)) with | O => w13_op | S n1 => match n1 return znz_op (word w12 (S (S n1))) with | O => w14_op | S n2 => match n2 return znz_op (word w12 (S (S (S n2)))) with | O => w15_op | S n3 => mk _ (mk _ (mk _ (make_op_aux n3))) end end end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1