proposition: Lemma rem_small_iff : forall a b, b~=0 -> (a rem b == a <-> abs a < abs b).
proof: Proof. intros a b ?. rewrite rem_eq, <- quot_small_iff by order. rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l. rewrite eq_sym_iff, eq_mul_0. tauto. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv