Proof of the Lax-Milgram Theorem

This page is dedicated to the formal proof in Coq of the Lax-Milgram Theorem.

The full code is downloadable here for Coq 8.8 or here for Coq 8.9 and above.

You may also want to browse the library by the index or by clicking the dependence graph: