Easy induction on directions

Stream: sphere eversion

[Patrick Massot]

Lemma 2.16 is essentially done modulo the key Lemma 2.11 and some easy sorries. The blueprint describes this as a "straightforward induction using lemma 2.11" but the Lean proof is still 100 lines long and I wanted to have it to make sure the data and properties flow well.

[Patrick Massot]

This proof needs cleaning of course, but it shows a lot of things work well.

[Patrick Massot]

It also generated quite a few accessible sorries, in case anyone is tired of Lie algebras.