proposition: Lemma Qmult_lt_1_compat: forall a b : Q, 1 < a -> 1 < b -> 1 < a * b.
proof: Proof. intros a b Ha Hb. destruct a,b. unfold Qlt, Qmult, QArith_base.Qnum, QArith_base.Qden in *. rewrite Pos2Z.inj_mul. rewrite Z.mul_1_l, Z.mul_1_r in *. apply Z.mul_lt_mono_nonneg. 2,4: assumption. 1,2: apply Pos2Z.is_nonneg. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool