as the Opam packages rocq-num-analysis-subset,<fnref n="20" /> rocq-num-analysis-algebra,<fnref n="21" /> and rocq-num-analysis-fem.<fnref n="22" /> The respective dependencies of these packages are shown in Figure 15. This development has led to a major reorganization of the previous coq-num-analysis package.

This formalization includes both generic and dedicated components. Among the generic components that could be reused for other projects, we find the finite families (a.k.a. vectors of a given size), affine spaces, substructures and restrictions of functions (that belong to the rocq-num-analysis-subset and rocq-num-analysis-algebra packages), but also multi-indices and multivariate polynomials of bounded degree. The dedicated components are the definition of what a finite element is with a precise Record including both values and requirements, and the instantiation of this record in the (popular) case of simplicial Lagrange finite elements.

## 10.2 Difficulties

The main difficulties we encountered are of two types: either due to mathematics or to formalization. As far as mathematics are concerned, the proofs are mostly based on [24], but with adaptation. For instance, we decided to work with almost no tools of analysis, and to employ purely affine arguments, only based on barycenters, for almost all steps of the construction of the simplicial Lagrange FE, see Sections 2.1 and 5, and [18]. We nevertheless relied on derivation in order to establish the linear independence of monomials in the space of multivariate polynomials, see Section 8.2.1.

The most difficult mathematical proof is the unisolvence of the Lagrange FE (see Section 9). It relies on a complex double induction with a polynomial factorization on a face. The formalization nicely follows the mathematical proof, but it still requires many steps, the connections being explained in Section 9.3. Another difficult mathematical proof is the freedom of monomials $(X^\alpha)_{\alpha \in A_k^d}$ (see Section 8.2.1). There exist several proof paths and we chose one with the greatest number of already formalized tools. So, based on the derivative of Coquelicot, we defined derivatives of multivariate polynomials at any order to derive $X^\alpha$ and proved that it is a linearly independent family.

Another kind of difficulty is that of formalization choices. Given a mathematical object, how can we define it in Rocq, so that it is usable and even user-friendly? An example is the multi-indices and more precisely the $A_k^d$'s (see Section 8.1.1), that can be sets, or lists, but we chose to make them finite families of the expected size and we proved an injectivity property. There are several ways to build them (with different orderings), and we chose what we called the grsymlex ordering, forcing the definition to fit this ordering. Contrary to mathematics, we made heavy use of the indexing of the multi-indices.

Another example is how to formally handle substructures. We have several subsets (such as polynomials, face hyperplanes) that preserve the algebraic structure of their support type. For instance, functions to $\mathbb{R}$ are a ModuleSpace, and so are polynomials. This subspace can be represented as a predicate $E \to \text{Prop}$ and the properties by an assumption. But from these, we can also define, with a dependent type, a set that can be instantiated as ModuleSpace itself. This is formalized and was used at one point (notably for unisolvence), but it proved less practical than handling subsets as additional parameters of, for instance, bijectivity, see Section 4.1.

A last example is the definition of affine spaces (see Section 4.3). This is a known geometric object (such as a hyperplane, shifted from the origin), but it ended up creating formalization hardships. The reason is that of canonical structures and the fact that there may be several paths to create such a structure. Consider the example of Figure 14 that describes the eight paths to build the fact that $\mathbb{R}^d$ is an instance of the AffineSpace structure. The mechanism of the canonical structures forces us to choose one of these paths (the blue one), but the path we need may be different depending on the proof at stake (e.g. a ModuleSpace instance). It is of course much worse in the case of $(\mathbb{R}^d)^{d+1}$ which is very common in our application (for the vertices of the geometrical

<footnote n="20">²⁰https://rocq-prover.org/p/rocq-num-analysis-subset/2.0.0</footnote>

<footnote n="21">²¹https://rocq-prover.org/p/rocq-num-analysis-algebra/2.0.0</footnote>

<footnote n="22">²²https://rocq-prover.org/p/rocq-num-analysis-fem/2.0.0</footnote>
element, i.e. $d + 1$ affinely independent points in $\mathbb{R}^d$). For a given definition on an affine space, such as *barycenter* or the predicate *aff_indep*, we add another definition with the suffix _ms_ equal to the preceding one, but typing only on a module space. This means duplicating some code, but helps choose the canonical structure path we need in several proofs.

<figure><img src="image_16.png" /><figcaption>Figure 14: Various ways to equip $\mathbb{R}^d$ with the affine space structure.</figcaption></figure>

Double-edged boxes denote actual instances of canonical structures in the Rocq system for $\mathbb{R}$, that is to say possible terminal points for the canonical structure search. Rectangular boxes denote the intent to equip a space (either $\mathbb{R}$ or $\mathbb{R}^d$) with an algebraic structure. Arrows correspond to generic canonical structures in our library, or in the *Coquelicot* library (when there is no link annotation). Names are abbreviated, *Ring_AS* actually means *Ring_AffineSpace*, an instance of *AffineSpace*, and *fct_MS* means *fct_ModuleSpace*, an instance of *ModuleSpace*. Then, the possibilities are all the paths from the wanted space and algebraic structure to a double-edged box.

For instance, there is only one way to equip $\mathbb{R}^d$ with the ring structure: by applying the *fct_Ring* canonical structure. $\mathbb{R}^d$ is then of type *fct_Ring* [0..d) *R_Ring*, which is an instance of *Ring*. This is automatic.

For the module space $\mathbb{R}^d$, there is a true diamond problem, with two distinct mathematical interpretations: either $\mathbb{R}^d$ is a module space over itself (*Ring_ModuleSpace* (*fct_Ring* [0..d) *R_Ring*)), or it is the regular module over $\mathbb{R}$ (*fct_ModuleSpace* [0..d) (*Ring_ModuleSpace* *R_Ring*)). But, there is also a third path, *fct_ModuleSpace* [0..d) *R_ModuleSpace*, which is the direct one, and is automatic.

Finally, for the affine space $\mathbb{R}^d$, there are eight distinct paths, the chosen one being the blue one. Again, the automatic path is the shortest one *fct_AffineSpace* [0..d) *R_AffineSpace* (blue arrows). But this path prevents us from seeing $\mathbb{R}^d$ as a *ModuleSpace*, preventing us from using some lemmas.

On top of all this complexity, affine spaces can also be mathematically equipped with a module space structure by choosing some origin and making it the zero vector. Fortunately, our proofs were not based on such construction, as it makes Rocq loop.

## 10.3 Design Choices

Now let us discuss our design choices. First, as explained in Section 3.4, we rely on several axioms, including classical logic. Given the mathematical proofs we want to formalize, this seems the best choice, as we want our statements to be similar to the mathematical ones. For instance, constructive analysis can lead to the statement $\neg\neg(\exists x \in \neg\neg P)$ instead of $\exists x \in P$, and that would not convince mathematicians of the maturity of our tools. We therefore preferred more understandable statements using classical logic.

A weakness of our formalization is that there are not enough requirements for the geometric element $K$ in the record type *FE*. It can be empty, or have an empty interior while this is usually forbidden in mathematics. Note that most of the constructed finite elements (in Sections 6 and 9) are suitable as the simplex $K$ is built from affinely independent vertices. A solution would be to require that a nonempty ball is included in $K$, but another appealing solution would be to build $K$ by a regular-enough function from reference vertices (be they simplex or cuboid reference
vertices). In the record, the vertices would be replaced by the function and the rest of the record
would be kept (unisolvence included) and most of this development would still apply, a notable
exception being the geometric transformation of a FE of Section 7.4. This perspective would also
allow us to deal with general hexahedra in 3D, whose faces are not necessarily planar and that
are not convex in general. Such nonconvex geometric elements can be used for instance in metal
forming [27].

<figure><img src="image_17.png" /><figcaption>Figure 15: Dependency graph, including the literature (in green), our contributions presented in this article (in yellow), and perspectives (in blue). Plain arrows are current dependencies between libraries, while dotted arrows are expected dependencies.</figcaption></figure>

**10.4 Perspectives**

A straightforward perspective is to consider cuboid finite elements and their properties. This will
require to factorize part of our development between simplex and cuboid finite elements. Cuboid
Lagrange finite elements are often defined as the tensorization of 1D Lagrange FE (i.e. taking $\mathbb{P}_k^1$
for each variable). Their unisolvence proof would be simpler and by induction on the dimension
only. What is more delicate is the fact that the geometric transformation is no longer affine in
general, see [24, Sec. 13.5].

Another important and challenging perspective is to handle face or edge elements, i.e. finite
elements of dimension $l$ that live in $\mathbb{R}^d$ with $l < d$ (typically $l = d - 1$). They can be used to
apply the boundary conditions of the PDE, but also for the treatment of fractures [39], or for the
boundary finite element methods, see for instance [35] and references therein. These boundary
elements do not fit in our formalization so far.

It would be also interesting to extend the record FE to finite elements whose approximation
space $P_{\text{approx}}$ takes its value in $\mathbb{R}^q$, with $q \ge 1$ (often $q = 1$ or $q = d$). This is a necessary step for
the construction of Raviart-Thomas flux FE [24, Chap. 14], that require a significant development
of integral, differential calculus and geometry components (such as face integrals, normals, and
non-affine geometric transforms).
More than other finite elements, we have several long-term perspectives described in Figure 15. We want to formally prove the finite element method, meaning the full algorithm to solve a PDE. As explained in Section 2.3, the PDE is solved on each finite element and glued together, the FEM guaranteeing the continuity of the computed solution. Therefore, we need to formalize Sobolev spaces (and prove they are Hilbert spaces).

The ultimate goal is to guarantee some (part of a) library implementing the finite element method, such as XLiFE++.<fnref n="23" /> It will be a different kind of proofs: more than proving the finite element method as a mathematical algorithm, it requires to prove it complies with the C++ program. A specific point out of the literature is to ensure that the floating-point errors do not mess too much with the results, relying on automatic provers or on the Flocq library [5].

## Acknowledgments

The authors thank Alexandre Ern, Guillaume Melquiond, and Pierre Rousselin for fruitful discussions about proof details, canonical structures, and notations. The authors are also thankful to David Hamelin for his help in tuning the CI and about the Nix package manager.

This work was partly supported by the European Research Council (ERC) under the European Union's Horizon 2020 Research and Innovation Programme – Grant Agreement n°810367.

## Bibliography

[1] Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, and Pierre-Yves Strub. Classical analysis with Coq. The 9th Coq Workshop, 2018. URL https://easychair.org/smart-slide/slide/n3pK.

[2] Ivo Babuška and Theofanis Strouboulis. *The finite element method and its reliability*. Numerical Mathematics and Scientific Computation. The Clarendon Press, Oxford University Press, New York, 2001. URL https://doi.org/10.1093/oso/9780198502760.001.0001.

[3] Ivo Babuška and J. Osborn. Eigenvalue problems. In *Finite Element Methods (Part 1)*, volume 2 of *Handbook of Numerical Analysis*, pages 641–787. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80042-0.

[4] Yves Bertot. Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs. In Bernd Fischer and Tarmo Uustalu, editors, *Proc. of the 15th Internat. Colloquium on Theoretical Aspects of Computing (ICTAC 2018)*, pages 3–10, Cham, 2018. Springer. URL https://doi.org/10.1007/978-3-030-02508-3_1.

[5] Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In *Proc. of the IEEE 20th Symposium on Computer Arithmetic (ARITH 2020)*, pages 243–252, Los Alamitos, 2011. IEEE. URL https://doi.org/10.1109/ARITH.2011.40.

[6] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. *J. Autom. Reason.*, 50(4):423–456, 2013. URL https://doi.org/10.1007/s10817-012-9255-4.

[7] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. *Math. Comput. Sci.*, 9(1):41–62, 2015. URL https://doi.org/10.1007/s11786-014-0181-1.

<footnote n="23">²³https://xlifepp.pages.math.cnrs.fr/</footnote>
[8] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax–Milgram theorem. In Proc. of the 6th ACM SIGPLAN Internat. Conf. on Certified Programs and Proofs (CPP 2017), pages 79–89, New York, 2017. Association for Computing Machinery. URL https://doi.org/10.1145/3018610.3018625.

[9] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. J. Autom. Reason., 66 (2):175–213, 2022. URL https://doi.org/10.1007/s10817-021-09612-0.

[10] Sylvie Boldo, François Clément, and Louise Leclerc. A Coq formalization of the Bochner integral. Research Report RR-9456, Inria, 2022. URL https://inria.hal.science/hal-03516749/.

[11] Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. A Coq formalization of Lebesgue induction principle and Tonelli's theorem. In M. Chechik, JP. Katoen, and M. Leucker, editors, Proc. of the 25th Internat. Symp. on Formal Methods (FM 2023), volume 14000 of LNCS, pages 39–55, Cham, 2023. Springer. URL https://doi.org/10.1007/978-3-031-27481-7_4.

[12] Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, and Pierre Rousselin. Teaching divisibility and binomials with Coq. In Julien Narboux, Walther Neuper, and Pedro Quaresma, editors, Proc. of the 13th Internat. Workshop on Theorem proving components for Educational software (ThEdu 2024), volume 419 of EPTCS, pages 124–139, 2024. URL https://doi.org/10.48550/arXiv.2404.12676.

[13] Suzanne C. Brenner and L. Ridgway Scott. The Mathematical Theory of Finite Element Methods, volume 15 of Texts in Applied Mathematics. Springer, New York, 3rd edition, 2008. URL https://doi.org/10.1007/978-0-387-75934-0.

[14] Haïm Brezis. Analyse fonctionnelle. Collection Mathématiques Appliquées pour la Maîtrise. [Collection of Applied Mathematics for the Master’s Degree]. Masson, Paris, 1983. URL https://www.dunod.com/sciences-techniques/analyse-fonctionnelle-theorie-et-applications-0. In French.

[15] P. G. Ciarlet and P. A. Raviart. General Lagrange and Hermite interpolation in Rn with applications to finite element methods. Arch. Ration. Mech. Anal., 46(4):177–199, 1972. URL https://doi.org/10.1007/BF00252458.

[16] Philippe G. Ciarlet. Basic error estimates for elliptic problems. In Finite Element Methods (Part 1), volume 2 of Handbook of Numerical Analysis, pages 17–351. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80039-0.

[17] Philippe G. Ciarlet. The Finite Element Method for Elliptic Problems, volume 40 of Classics in Applied Mathematics. Society for Industrial and Applied Mathematics (SIAM), Philadelphia, 2002. URL https://doi.org/10.1137/1.9780898719208. Reprint of the 1978 original [North-Holland, Amsterdam].

[18] François Clément and Vincent Martin. Finite element method. Detailed proofs to be formalized in Coq. Research Report RR-9557, Inria, 2024. URL https://inria.hal.science/hal-04713897/. Release 1.0 (v1).

[19] David A. Cox, John Little, and Donal O’Shea. Ideals, Varieties, and Algorithms. Undergraduate Texts in Mathematics. Springer, Cham, 2015. URL https://doi.org/10.1007/978-3-319-16721-3.

[20] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Proc. of the 25th Internat. Conf. on Automated Deduction (CADE 2015), volume 9195 of LNCS, pages 378–388, Cham, 2015. Springer. URL https://doi.org/10.1007/978-3-319-21401-6_26.
[21] Elif Deniz, Adnan Rashid, Osman Hasan, and Sofiène Tahar. On the formalization of the heat conduction problem in HOL. In Kevin Buzzard and Temur Kutsia, editors, *Proc. of the 15th Internat. Conf. on Intelligent Computer Mathematics (CICM 2022)*, volume 13467 of LNCS, pages 21–37, Cham, 2022. Springer. URL https://doi.org/10.48550/arXiv.2208.06642.

[22] Jean-François Dufourd and Yves Bertot. Formal study of plane Delaunay triangulation. In Matt Kaufmann and Lawrence C. Paulson, editors, *Proc. of the 1st Internat. Conf. on Interactive Theorem Proving (ITP 2010)*, pages 211–226, Berlin - Heidelberg, 2010. Springer. URL https://doi.org/10.1007/978-3-642-14052-5_16.

[23] Alexandre Ern and Jean-Luc Guermond. *Theory and Practice of Finite Elements*, volume 159 of *Applied Mathematical Sciences*. Springer, New York, 2004. URL https://doi.org/10.1007/978-1-4757-4355-5.

[24] Alexandre Ern and Jean-Luc Guermond. *Finite Elements I. Approximation and Interpolation*, volume 72 of *Texts in Applied Mathematics*. Springer, Cham, 2021. URL https://doi.org/10.1007/978-3-030-56341-7.

[25] Alexandre Ern and Jean-Luc Guermond. *Finite Elements II. Galerkin Approximation, Elliptic and Mixed PDEs*, volume 73 of *Texts in Applied Mathematics*. Springer, Cham, 2021. URL https://doi.org/10.1007/978-3-030-56923-5.

[26] Alexandre Ern and Jean-Luc Guermond. *Finite Elements III. First-Order and Time-Dependent PDEs*, volume 74 of *Texts in Applied Mathematics*. Springer, Cham, 2021. URL https://doi.org/10.1007/978-3-030-57348-5.

[27] J.L.M. Fernandes and P.A.F. Martins. All-hexahedral remeshing for the finite element analysis of metal forming processes. *Finite. Elem. Anal. Des.*, 43(8):666–679, 2007. ISSN 0168-874X. URL https://doi.org/10.1016/j.finel.2007.02.001.

[28] Miguel A. Fernández, Jean-Frédéric Gerbeau, and Vincent Martin. Numerical simulation of blood flows through a porous interface. *M2AN Math. Model. Numer. Anal.*, 42(6):961–990, 2008. URL https://doi.org/10.1051/m2an:2008031.

[29] Hiroshi Fujita and Takashi Suzuki. Evolution problems. In *Finite Element Methods (Part 1)*, volume 2 of *Handbook of Numerical Analysis*, pages 789–928. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80043-2.

[30] Herman Geuvers and Milad Niqui. Constructive reals in Coq: Axioms and categoricity. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, *Proc. of the Internat. Workshop on Types for Proofs and Programs (TYPES 2000)*, volume 2277 of LNCS, pages 79–95, Berlin - Heidelberg, 2002. Springer. URL https://doi.org/10.1007/3-540-45842-5_6.

[31] Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A small scale reflection extension for the Coq system. Research Report RR-6455, Inria, 2008. URL https://inria.hal.science/inria-00258384/.

[32] Bernard Gostiaux. *Cours de mathématiques spéciales - 1. Algèbre* [Lecture Notes in Special Mathematics - 1. Algebra]. Mathématiques. Presses Universitaires de France, Paris, 1993. URL https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre. In French.

[33] Bernard Gostiaux. *Cours de mathématiques spéciales - 4. Géométrie affine et métrique* [Lecture Notes in Special Mathematics - 4. Affine and metric geometry]. Mathématiques. Presses Universitaires de France, Paris, 1995. URL https://www.puf.com/cours-de-mathematiques-speciales-tome-4-geometrie-affine-et-metrique. In French.
[34] Fabian Immler and Johannes Hölzl. Numerical analysis of ordinary differential equations in Isabelle/HOL. In Lennart Beringer and Amy P. Felty, editors, *Proc. of the 3rd Internat. Conf. on Interactive Theorem Proving (ITP 2012)*, volume 7406 of LNCS, pages 377–392, Berlin - Heidelberg, 2012. Springer. URL https://doi.org/10.1007/978-3-642-32347-8_26.

[35] Patrick Joly and Jerónimo Rodríguez. Mathematical aspects of variational boundary integral equations for time dependent wave propagation. *J. Integral Equ. Appl.*, 29(1):137–187, 2016. URL https://doi.org/10.1216/JIE-2017-29-1-137.

[36] Marie Kerjean, Micaela Mayero, and Pierre Rousselin. Maths with coq in l1, a pedagogical experiment. In Julien Narboux, Walther Neuper, and Pedro Quaresma, editors, *Proc. of the 13th Internat. Workshop on Theorem proving components for Educational software (ThEdu 2024)*, volume 419 of EPTCS, pages 112–123, 2024. URL https://doi.org/10.48550/arXiv.2505.05990.

[37] Assia Mahboubi and Enrico Tassi. Canonical structures for the working Coq user. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, *Proc. of the 4th Internat. Conf. on Interactive Theorem Proving (ITP 2013)*, volume 7998 of LNCS, pages 19–34, Berlin - Heidelberg, 2013. Springer. URL https://doi.org/10.1007/978-3-642-39634-2_5.

[38] Assia Mahboubi and Enrico Tassi. *Mathematical Components*. Zenodo, Genève, 2020. URL https://doi.org/10.5281/zenodo.7118596.

[39] Vincent Martin, Jérôme Jaffré, and Jean E. Roberts. Modeling fractures and barriers as interfaces for flow in porous media. *SIAM J. Sci. Comput.*, 26(5):1667–1691, 2005. URL https://doi.org/10.1137/S1064827503429363.

[40] Micaela Mayero. *Formalisation et automatisation de preuves en analyses réelle et numérique [Formalization and Proof Automation in Real and Numerical Analysis]*. Thèse de Doctorat, Université Paris VI, 2001. URL https://www-lipn.univ-paris13.fr/%7Emayero/publis/these-mayero.ps.gz. In French.

[41] Laura Meikle and Jacques Fleuriot. Automation for geometry in Isabelle/HOL. In Renate A. Schmidt, Stephan Schulz, and Boris Konev, editors, *Proc. of the 2nd Workshop on Practical Aspects of Automated Reasoning (PAAR 2010)*, volume 9 of EPiC Series in Computing, pages 84–94, Bramhall, UK, 2012. EasyChair. URL https://doi.org/10.29007/r5k7.

[42] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. *Isabelle/HOL—A Proof Assistant for Higher-Order Logic*, volume 2283 of LNCS. Springer, Berlin - Heidelberg, 2002. URL https://doi.org/10.1007/3-540-45949-9.

[43] Sora Otsuki, Pauline N. Kawamoto, and Hiroshi Yamazaki. A simple example for linear partial differential equations and its solution using the method of separation of variables. *Formaliz. Math.*, 27(1):25–34, 2019. URL https://doi.org/10.2478/forma-2019-0003.

[44] Christine Paulin-Mohring. *Définitions Inductives en Théorie des Types [Inductive Definitions in Type Theory]*. Habilitation à diriger les recherches, Université Claude Bernard Lyon I, 1996. URL https://hal.science/tel-00431817/. In French.

[45] Alfio Quarteroni and Alberto Valli. *Numerical approximation of partial differential equations*, volume 23 of Springer Series in Computational Mathematics. Springer, Berlin - Heidelberg, 1994. URL https://doi.org/10.1007/978-3-540-85268-1.

[46] Jean E. Roberts and Jean-Marie Thomas. Mixed and hybrid methods. In *Finite Element Methods (Part 1)*, volume 2 of Handbook of Numerical Analysis, pages 523–639. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80041-9.
[47] Vincent Semeria. Nombres réels dans Coq [Real numbers in Coq]. In Zaynah Dargaye and Yann Regis-Gianas, editors, *Actes des 31es Journées Francophones des Langages Applicatifs (JFLA 2020)*, pages 104–111. IRIF, 2020. URL https://inria.hal.science/hal-02427360/. In French.

[48] Mohit Tekriwal, Karthik Duraisamy, and Jean-Baptiste Jeannin. A formal proof of the Lax equivalence theorem for finite difference schemes. In A. Dutle, M.M. Moscato, L. Titolo, C.A. Muñoz, and I. Perez, editors, *Proc. of the 13th Internat. Symp. NASA Formal Methods (NFM 2021)*, volume 12673 of LNCS, Cham, 2021. Springer. URL https://doi.org/10.1007/978-3-030-76384-8_20.

[49] Lars B. Wahlbin. Local behavior in finite element methods. In *Finite Element Methods (Part 1)*, volume 2 of *Handbook of Numerical Analysis*, pages 353–522. Elsevier Science Publishers B.V., North-Holland, 1991. URL https://doi.org/10.1016/S1570-8659(05)80040-7.

[50] Benjamin Werner. *Une théorie des constructions inductives* [*A Theory of Inductive Constructions*]. Thèse de Doctorat, Université Paris VII, 1994. URL https://hal.science/tel-00196524v2. In French.

[51] O. C. Zienkiewicz, R. L. Taylor, and J. Z. Zhu. *The Finite Element Method: its Basis and Fundamentals*. Elsevier/Butterworth Heinemann, Amsterdam, 7th edition, 2013. URL https://doi.org/10.1016/B978-1-85617-633-0.00001-0.
<figure><img src="image_18.png" /></figure>

RESEARCH CENTRE
Centre Inria de Saclay

Bâtiment Alan Turing
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
91120 Palaiseau

Publisher
Inria
Domaine de Voluceau - Rocquencourt
BP 105 - 78153 Le Chesnay Cedex
inria.fr

ISSN 0249-6399