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