proposition: Lemma ndouble_wf: forall x sc, wfe x -> wft sc -> wfe (fst (ndouble sc x)) /\ wft (snd (ndouble sc x)).
proof: Proof. intros x; case x; clear x; auto. intros x1 y1 z1 sc (wfx1,(wfy1, wfz1)) wfsc; simpl; auto. repeat (case neq; repeat split; simpl; nw; auto). Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod