proposition: Lemma rem_nonpos : forall a b, b~=0 -> a <= 0 -> a rem b <= 0.
proof: Proof. intros a b Hb Ha. apply opp_nonneg_nonpos. apply opp_nonneg_nonpos in Ha. rewrite <- rem_opp_l by trivial. now apply rem_nonneg. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv