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