proposition: Lemma mod_sign_mul : forall a b, b~=0 -> 0 <= (a mod b) * b.
proof: Proof. intros a b **. destruct (lt_ge_cases 0 b). - apply mul_nonneg_nonneg; destruct (mod_pos_bound a b); order. - apply mul_nonpos_nonpos; destruct (mod_neg_bound a b); order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv