Translate lesson 2 of the Rocq tutorial into Lean#806

stepchowfun wants to merge 1 commit intomainstepchowfun/proofs:mainfrom

lesson2-leanstepchowfun/proofs:lesson2-leanCopy head branch name to clipboard