proposition: Lemma uncurry_uniform `{!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: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.orders HoTT.Classes.implementations.peano_naturals HoTT.Classes.implementations.natpair_integers HoTT.Classes.theory.groups HoTT.Classes.theory.integers HoTT.Classes.theory.dec_fields HoTT.Classes.orders.dec_fields HoTT.Classes.orders.sum HoTT.Classes.theory.rationals HoTT.Classes.orders.lattices HoTT.Classes.implementations.assume_rationals HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_tac