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