lipschitz_nonexpanding@{} `{!Lipschitz f 1} : NonExpanding f. Proof. red. intros e x y E;rewrite <-(left_identity e). apply (lipschitz f 1 E). Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.