proposition: Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r -> p / r <= p / q.
proof: Proof. intros; apply Z.div_le_compat_l; intuition auto using Z.lt_le_incl. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms