proposition: Lemma rem_bound_abs : forall a b, b~=0 -> abs (a rem b) < abs b.
proof: Proof. intros. rewrite <- rem_abs; trivial. apply rem_bound_pos. - apply abs_nonneg. - now apply abs_pos. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv