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.

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