proposition: Lemma le_0_eq x: x <= 0%Qnn -> x == 0%Qnn.
proof: Proof. split. assumption. apply le_0. Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program