rounded_le@{i j} := ltac:(first [exact @rounded_le'@{j i Ularge}| exact @rounded_le'@{j i Ularge j}| exact @rounded_le'@{i j}]). Arguments rounded_le {A _ _} e u v _ d _. Section close_prod. Universe UA UB i. Context (A:Type@{UA}) (B:Type@{UB}) `{Closeness A} `{Closeness B} `{forall e, is_mere_relation A (close e)} `{forall e, is_mere_relation B (close e)}. Global Instance close_prod@{} : Closeness@{i} (A /\ B) := fun e x y => close e (fst x) (fst y) /\ close e (snd x) (snd y). Global Instance close_prod_refl@{} `{forall e, Reflexive (close (A:=A) e)} `{forall e, Reflexive (close (A:=B) e)} : forall e, Reflexive (close (A:=A /\ B) e). Proof. intros e;split;reflexivity. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.