We will talk about using Lean to provide guarantees about data structures which are useful real world software. In particular, we will look at arrays and vectors. The arrays require…