proposition: Lemma nmulw: forall x y, wft x -> wft y -> wft (x ** y).
proof: Proof. intros x y Hx Hy. unfold wft. pattern (z2Z (x ** y)) at 2; rewrite (nmulz Hx Hy). unfold ZEll.nmul; rewrite z2ZN. rewrite Zmod_mod; auto. apply (nmulz Hx Hy). Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod