map2_lipschitz' `{!Rounded C} `{!Rounded D} Lf Lg `{!Lipschitz f Lf} `{!Lipschitz g Lg} : Lipschitz (map2 f g) (join Lf Lg). Proof. intros e u v xi. split;simpl. - apply rounded_le with (Lf * e). + apply (lipschitz _ _),xi. + apply (order_preserving (.* ' e)). apply join_ub_l. - apply rounded_le with (Lg * e). + apply (lipschitz _ _),xi. + apply (order_preserving (.* ' e)). apply join_ub_r. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.