LagP1_is_non_neg and LagQ1_is_non_neg lemmas.
Try to prove T_geom_is_affine.

Prove is_linear_mapping_f_scal_l
	& comb_lin_linear_mapping_compat_l lemmas.

Add some comments.

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.