proposition: Lemma Qle_shift_inv_r : forall b c, 0 < b -> 1 <= c*b -> /b <= c.
proof: Proof. intros b c Hc H. setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l). change (1/b <= c). apply Qle_shift_div_r; assumption. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool