proposition: Lemma Z_mod_nonneg_nonneg : forall a b, 0 <= a -> 0 <= b -> 0 <= a mod b.
proof: Proof. destruct b; intros; now (rewrite Zmod_0_r + apply Z_mod_lt). Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms