proof of Lazard Theorem

Stream: maths

[Wenrong Zou]

I am trying to formalize the Lazard Theorem for one dimensional formal group laws. There are several proofs mentioned in the link above (and also a proof in the Hazewinkel 's book Formal Group Laws and Applications). I was wondering which proof I should follow or which proof is better to formalize. We can assume that we have enough APIs for formal group law, including functional equation lemma in Hazewinkel's book.

Assuming this result, we are able to say that the functor FGL : CommRingCat ⥤ Type is corepresented by some formal group law F over Lazard ring L.

Thanks in advance!