proposition: Lemma Qopp_Qlt_0_l (x: Q): 0 < -x <-> x < 0.
proof: Proof. split. rewrite <- (Qopp_opp x) at 2. apply (Qopp_lt_compat 0 (-x)). apply (Qopp_lt_compat x 0). 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