`{!Rounded A} `{!Rounded B} (f : A -> B -> C) mu mu' `{!forall x, Uniform (f x) mu} `{!forall y, Uniform (fun x => f x y) mu'} : Uniform (uncurry f) (fun e => meet (mu (e/2)) (mu' (e/2))). Proof. intros e [u1 u2] [v1 v2] [xi1 xi2]. simpl in *. rewrite (pos_split2 e). apply (triangular _ (f u1 v2)). - apply (uniform (f u1) _). eapply rounded_le. + exact xi2. + apply meet_lb_l. - apply (uniform (fun v => f v v2) _). eapply rounded_le. + exact xi1. + apply meet_lb_r. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.