close_prod_rounded@{j} := ltac:(first [exact @close_prod_rounded'@{j j j j j}| exact @close_prod_rounded'@{j j}| exact @close_prod_rounded'@{j j j}]).
Require Import Import NatPair.Instances. Import Quoting.Instances.