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.

WIP: Lemma bigop_op_idx.

Comment parts of Finite_dim.v to compile

prove kronecker_bigop_scal_in_r, kronecker_bigop_scal_out_r,
kronecker_bigop_l, kronecker_bigop_r lemmas.

move sum_pn_scal lemma to sum_pn.v

Try to make Pval a coercion (try with Pol' instead of Pol)
Patch com_lin in files

Start using comb_lin.

File should be renamed comb_lin.v.