proposition: Theorem spec_mul : forall x y, [mul x y] = [x] * [y].
proof: Proof. intros x y. rewrite mul_fold. apply spec_iter_sym; clear x y. intros n x y. cbv zeta beta. rewrite spec_reduce, spec_succ_t, <- ZnZ.spec_mul_c; auto. apply spec_wn_mul. intros n m x y; unfold mulnm. rewrite spec_reduce_n. rewrite (spec_cast_l n m x), (spec_cast_r n m y). apply spec_muln. intros. rewrite Z.mul_comm; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen