proposition: Lemma nopp_wf: forall x, wfe x -> wfe (nopp x).
proof: Proof. intros x; case x; simpl nopp; auto. intros x1 y1 z1 [H1 [H2 H3]]; repeat split; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod