proposition: Lemma nsubw: 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 (nsubz Hx Hy). unfold ZEll.nsub; rewrite z2ZN. rewrite Zmod_mod; auto. apply (nsubz Hx Hy). Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod