Comment by varjag

It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.