proposition: Lemma BinopBound_le x y a b: (`a <= `b)%Q -> BinopBound x y a -> BinopBound x y b.
proof: Proof. Proof with auto. intros E B. revert B E. intros [v w xv yw r F] E. apply (is_binop_bound x y v w)... apply Qle_trans with (`r)... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program