proposition: Lemma BinopBound_assoc (n m p: T) (q: QnonNeg): BinopBound (is_bound n) (BinopBound (is_bound m) (is_bound p)) q -> BinopBound (BinopBound (is_bound n) (is_bound m)) (is_bound p) q.
proof: Proof. Proof with auto. intros [a b na [v w z x y E] c F]. apply BinopBound_le with (o_nn (o_nn a v) w). simpl. apply Qle_trans with (o (`a) (`y))... rewrite <- o_assoc. apply o_le_compat; split... apply is_binop_bound with (o_nn a v) w... apply is_binop_bound with a v... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program