proposition: Lemma Qinv_lt_contravar : forall a b : Q, 0 < a -> 0 < b -> (a < b <-> /b < /a).
proof: Proof. intros a b H H0. split. - intro H1. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. + apply H0. + rewrite <- (Qmult_inv_r a). * rewrite Qmult_comm. apply Qmult_lt_l. -- apply Qinv_lt_0_compat. apply H. -- apply H1. * intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). - intro H1. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). apply Qlt_shift_div_l. + apply Qinv_lt_0_compat. apply H0. + rewrite <- (Qmult_inv_r a). * apply Qmult_lt_l. -- apply H. -- apply H1. * intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool