proposition: Lemma rem_sign_mul : forall a b, b~=0 -> 0 <= (a rem b) * a.
proof: Proof. intros a b Hb. destruct (le_ge_cases 0 a). - apply mul_nonneg_nonneg; trivial. now apply rem_nonneg. - apply mul_nonpos_nonpos; trivial. now apply rem_nonpos. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv