proposition: Theorem Zdivide_Zdiv_lt_pos a b : 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b .
proof: Proof. intros H1 H2 H3. assert (0 < a) by (now transitivity 1). split. + apply Z.mul_pos_cancel_l with a; auto. rewrite <- Zdivide_Zdiv_eq; auto. + now apply Z.div_lt. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat