proposition: Lemma spec_wn_mul : forall n m x y, [wn_mul n m x y] = (eval n (S m) x) * ZnZ.to_Z y.
proof: Proof. intros; unfold wn_mul. generalize (spec_mul_add_n1 n m x y ZnZ.zero). case DoubleMul.double_mul_add_n1; intros q r Hqr. rewrite ZnZ.spec_0, Z.add_0_r in Hqr. rewrite <- Hqr. generalize (ZnZ.spec_eq0 q); destruct ZnZ.eq0; intros HH. rewrite HH; auto. simpl. apply spec_mk_t_w'. clear. rewrite spec_mk_t_w'. set (m' := S m) in *. unfold eval. rewrite nmake_WW. f_equal. f_equal. rewrite <- spec_mk_t. symmetry. apply spec_extend. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen