`{Rounded A} : forall d d' u v, close d u v -> close (d+d') u v. Proof. intros d d' u v xi;apply rounded. apply tr;exists d,d';auto. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.