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