proposition: Theorem add_rem: forall a b n, n~=0 -> 0 <= a*b -> (a+b) rem n == (a rem n + b rem n) rem n.
proof: Proof. intros a b n Hn Hab. rewrite add_rem_idemp_l, add_rem_idemp_r; trivial. - reflexivity. - destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]; destruct (le_0_mul _ _ (rem_sign_mul b n Hn)) as [(Hb',Hm)|(Hb',Hm)]; auto using mul_nonneg_nonneg, mul_nonpos_nonpos. + setoid_replace b with 0 by order. rewrite rem_0_l by order. nzsimpl; order. + setoid_replace b with 0 by order. rewrite rem_0_l by order. nzsimpl; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv