map2_continuous' `{!Rounded A} `{!Rounded B} `{!Continuous f} `{!Continuous g} : Continuous (map2 f g). Proof. intros u e. apply (merely_destruct (continuous f (fst u) e));intros [d1 E1]. apply (merely_destruct (continuous g (snd u) e));intros [d2 E2]. apply tr;exists (meet d1 d2). intros v xi. split;simpl. - apply E1. apply rounded_le with (meet d1 d2). + apply xi. + apply meet_lb_l. - apply E2. apply rounded_le with (meet d1 d2). + apply xi. + apply meet_lb_r. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.