work with cur_to_ref properties.

Work on cur_to_ref properties.

move the comment to FE.v

add is_affine_comb_lin_compat lemma. Still admitted.

remove sum_pn.v and poly_Mathcomp.v files

Try to prove T_geom_is_affine lemma (WIP).
Prove multiple lemmas of T_geom map.

Prouver LagPQ_is_non_neg mais faut plus d'hypothèses.
Changer l'énoncé de T_geom_is_affine.
Ajouter des notes en commentaires

Énoncer des lemmes pour LagP1 et LagQ1.

Work on other proofs of T_geom.

 and interp_op_local_cur_ref lemmas.
Add many Qsts as comments (HM : ).
So much cleaning has been done.

Un peu de renommage.

Plus passage Pol' -> Pol

and the one of Lagrange

Change the proofs of interpolation operator lemmas
with the use of comb_lin lemmas.
Put all the Poly_Lagrange_basis section in a separate file.
Refine the FE_Reference_Def section.

move kronecker_nat to sandbox.