proposition: Lemma range_div_pos: forall a b c d, 0 < d -> a <= b <= c -> a / d <= b / d <= c / d.
proof: Proof. intuition idtac. - apply (Z.div_le_mono _ _ _ H H1). - apply (Z.div_le_mono _ _ _ H H2). Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith