proposition: Lemma Qopp_Qlt_0_r (x: Q): -x < 0 <-> 0 < x.
proof: Proof. rewrite <- Qopp_Qlt_0_l, Qopp_opp. reflexivity. 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