proposition: Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a.
proof: Proof. intros a b b_ge_2 a_gt_0. apply Z.div_lt. - apply Z.gt_lt; exact a_gt_0. - apply (Z.lt_le_trans _ 2). + reflexivity. + apply Z.ge_le; exact b_ge_2. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms