proposition: Lemma nopp_correct: forall x, wfe x -> e2E x = ZEll.nopp exx.(vN) (e2E (nopp x)).
proof: Proof. intros x; case x; simpl; auto. intros x1 y1 z1 [H1 [H2 H3]]; apply f_equal3 with (f := ZEll.ntriple); auto. rewrite nsubz; auto. rewrite zc0. unfold ZEll.nsub, ninv; simpl. apply sym_equal. rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. rewrite <- Zopp_mult_distr_l. rewrite <- Zopp_plus_distr. rewrite Zmult_comm; rewrite Zplus_comm. rewrite <- Z_div_mod_eq_full. rewrite Z.opp_involutive; rewrite <- z2ZN. apply sym_equal; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod