proposition: Lemma Qle_dec x y: {Qle x y} + {~Qle x y}.
proof: Proof. intros. destruct (Qlt_le_dec y x); [right | left]; [apply Qlt_not_le |]; assumption. Defined.
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