proposition: Lemma binop_le_compat_l (x y z: T): x <= y -> binop x z <= binop y z.
proof: Proof. Proof with auto. unfold le. simpl. intros H q [v w yv zw r E] s rs. specialize (H _ yv). assert (o (`v) (`w) < `s) as os. apply Qle_lt_trans with (`r)... destruct (o_sneaky _ _ _ (proj2_sig _) (proj2_sig _) os). apply (is_binop_bound (is_bound x) (is_bound z)) with (v + from_Qpos x0)%Qnn w... apply H. simpl. rewrite Qplus_comm. rewrite <- Qplus_0_l at 1. apply Qplus_lt_l... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program