proposition: Theorem rem_rem: forall a n, n~=0 -> (a rem n) rem n == a rem n.
proof: Proof. intros a n **. pos_or_neg a; pos_or_neg n. - apply NZQuot.mod_mod; order. - rewrite <- ! (rem_opp_r _ n) by trivial. apply NZQuot.mod_mod; order. - apply opp_inj. rewrite <- !rem_opp_l by order. apply NZQuot.mod_mod; order. - apply opp_inj. rewrite <- !rem_opp_opp by order. apply NZQuot.mod_mod; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv