proposition: Lemma le_refl (x: T): x <= x.
proof: Proof. repeat intro. apply closed_le with q; auto. Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program