proposition: Lemma spec_muln: forall n (x: word _ (S n)) y, [Nn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [Nn n x] * [Nn n y].
proof: Proof. intros n x y; unfold to_Z. rewrite <- ZnZ.spec_mul_c. rewrite make_op_S. case ZnZ.mul_c; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen