[ooovi]

Integrating the proofs @mo271 and @theran worked on during the workshop:

• proving the lemma (hx : x ∉ convexHull R s) : IsFaceOf R ({x} : Set A) (convexHull R (insert x s)) using homogenization and a corresponding cone lemma
• using it to prove krein milman for polytopes inductively
• using that and homogenization for a nicer version of krein milman for FG cones

i'm not sure this is the approach we want. louis has done a lot of work to avoid the first use of homogenization here, but I'm not sure why we'd want to avoid it?

depends on #115 and #112 if we merge them the diff will look nice