proposition: Lemma Qlt_shift_div_r : forall a b c, 0 < b -> a < c*b -> a/b < c.
proof: Proof. intros a b c Hc H. apply Qnot_le_lt. intros H0. apply (Qlt_not_le _ _ H). apply Qmult_lt_0_le_reg_r with (/b). - apply Qinv_lt_0_compat. assumption. - setoid_replace (c*b/b) with (c) by (apply Qdiv_mult_l; auto with *). assumption. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool