proposition: Lemma Qdiv_flip_lt (x y : Q) : 0 < x -> x < y -> /y < /x.
proof: Proof. intros E1 E2. assert (0 < y) by now apply Qlt_trans with x. apply Qmult_lt_l with x; try assumption. apply Qmult_lt_l with y; try assumption. field_simplify. now try (unfold Qdiv; rewrite 2!Qmult_1_r). now apply Qneq_symmetry, Qlt_not_eq. now apply Qneq_symmetry, Qlt_not_eq. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List