proposition: Lemma map2_lipschitz' `{!Rounded C} `{!Rounded D} Lf Lg `{!Lipschitz f Lf} `{!Lipschitz g Lg} : Lipschitz (map2 f g) (join Lf Lg).
proof: 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.
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