Shouldn't the |bn-l| be |cn-l| in the last second line of [Sandwich Theorem](https://leanprover-community.github.io/format_lean/example/sandwich.html)? 
