proposition: Lemma nsubz: forall x y, wft x -> wft y -> z2Z (x -- y) = ZEll.nsub (vN exx) (z2Z x) (z2Z y).
proof: Proof. intros x y Hx Hy. unfold z2Z, nsub. rewrite (mop_spec.(sub_mod_spec) _ _ _ _ Hx Hy); auto. rewrite <- z2ZN; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod