proposition: Lemma nadd_correct: forall x y sc, wfe x -> wfe y -> wft sc -> e2E (fst (nadd sc x y)) = fst (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y) )/\ z2Z (snd (nadd sc x y)) = snd (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E 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. ftac. ftac. 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). rewrite nmulz; auto. 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