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