lipschitz_compose_nonexpanding_r' L {Eg : Lipschitz g L} {Ef : NonExpanding f} : Lipschitz (Compose g f) L. Proof. rewrite <-(left_identity L),commutativity. apply _. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.