proposition: Lemma ndouble_correct: forall x sc, wfe x -> wft sc -> e2E (fst (ndouble sc x)) = fst (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x))/\ z2Z (snd (ndouble sc x)) = snd (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x)).
proof: Proof. intros x; case x; clear x; auto. intros x1 y1 z1 sc (wfx1,(wfy1, wfz1)) wfsc; simpl. ftac. simpl; split; auto. repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto). simpl; split; auto. repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz || rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto). Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod