proposition: Lemma Qle_shift_div_l : forall a b c, 0 < c -> a*c <= b -> a <= b/c.
proof: Proof. intros a b c Hc H. apply Qmult_lt_0_le_reg_r with (c). - assumption. - setoid_replace (b/c*c) with (c*(b/c)) by apply Qmult_comm. rewrite Qmult_div_r; try assumption. auto with *. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool