nonexpanding_lipschitz@{} `{!NonExpanding f} : Lipschitz f 1 := ltac:(first [exact nonexpanding_lipschitz'@{Ularge}| exact nonexpanding_lipschitz'@{}]).
Require Import Import NatPair.Instances. Import Quoting.Instances.