proposition: Lemma spec_rem : forall x y, to_Z (rem x y) = Z.rem (to_Z x) (to_Z y).
proof: Proof. intros x y. unfold rem. rewrite spec_eqb, spec_0. case Z.eqb_spec; intros Hy. rewrite Hy. now destruct (to_Z x). destruct x as [x|x], y as [y|y]; simpl in *; symmetry; rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy; rewrite NN.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd; trivial; apply Z.rem_mod_nonneg; generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig