Generalize and move poly_Lagrange.comb_lin_comb_lin to ModuleSpace_compl.comb_lin2.

ModuleSpace_compl:
Remove useless comb_lin2_l.
Rename comb_lin2_r -> comb_lin2_alt (+ simplify proof).

matrix, AffineSpace, Finite_dim:
Propagate new API (from ModuleSpace_compl).

Move A_d_k_kron from poly_Lagrange to multi_index.
Remove useless poly_Lagrange.comb_lin_itemF_aux (use comb_lin_itemF_l instead).

modif de A_d_k notamment

Add binom_sym_alt, binom_rising_sum{1,2}.
Remove old def binom1 and results.

multi_index:
Proofs of C_d_k_aux, C_d_k_aux2 and A_d_k_aux.
TODO: fix C_d_k_aux and adpat def C_d_k.

WIP: has_dim_inter, lm_sub_is_surj_dim_equiv.

Move stuff around (proofs actually needs commutativity of the scalar ring,
  thus are stated later with the ring of reals R_Ring).
WIP: has_dim_monot, has_dim_eq,
     has_dim_inter, has_dim_inter_lb_l, has_dim_inter_l.
Add and prove dim_monot, dim_eq,
              dim_inter, dim_inter_lb_l, dim_inter_l,
              has_dim_inter_lb_r, has_dim_inter_r,
              dim_inter_lb_r, dim_inter_r.

Finite_dim:
Add and prove lm_sub_is_inj_dim_equiv, lm_sub_is_bij_dim_equiv.
WIP: lm_sub_is_surj_dim_equiv, is_inj_is_surj_equiv.

      pour une fonction affine de R^n vers R^d

  pour une fonction affine de R^n vers R^d

Make separate section for defs Ker_sub/Rg_sub.

Finite_dim:
Fix is_linear_mapping_is_basis_compat (is_bij -> is_inj).
Cleaning of dead code.
Resurrect rank_thm (WIP).
Fix is_inj_is_surj_equiv (WIP), is_bij_is_inj_equiv, is_bij_is_surj_equiv
    (add hypothesis on PF : dim PF = dim PE).

FE_simplex:
Propagate new API (from Finite_dim).

 under the Facts_R section, to be moved.

Rename len_n0F_extendF -> lenPF_n0F_extendF.

Sub_struct:
Rename is_inj_Ker_sub_zero -> lm_sub_is_inj_rev,
       Ker_sub_zero_is_inj -> lm_sub_is_inj,
       Ker_sub_zero_is_inj_equiv -> lm_sub_is_inj_equiv,
       is_surj_Rg_sub_full -> lm_sub_is_surj_rev,
       Rg_sub_full_is_surj -> lm_sub_is_surj,
       Rg_sub_full_is_surj_equiv -> lm_sub_is_surj_equiv,
       is_bij_Ker_sub_zero_Rg_sub_full -> lm_sub_is_bij_rev,
       Ker_sub_zero_Rg_sub_full_is_bij -> lm_sub_is_bij,
       Ker_sub_zero_Rg_sub_full_is_bij_equiv -> lm_sub_is_bij_equiv.

FE_simplex:
Propagate new API (from Sub_struct).

Add and prove compatible_as_ms_equiv_R (shortcut).

Finite_dim:
Proof of aff_span_compatible_as (needs R_Ring, moved below).
Remove useless shortcuts for affine spaces on R.

Add and prove frameF_inclF.

Finite_dim:
Move stuff around.
Make some arguments implicit.
Add and prove is_free_dim_is_generator, is_generator_dim_is_free, dim_is_free_generator_equiv,
              is_aff_basis_is_aff_gen, is_aff_basis_is_aff_indep,
              is_aff_gen_nonempty, is_aff_basis_nonempty, has_aff_dim_is_nonempty,
              has_aff_dim_lin, has_aff_dim_lin_rev, has_dim_aff, has_dim_aff_rev,
              *aff_*_R, is_aff_gen_dim_is_aff_basis, is_aff_gen_dim_is_aff_indep,
              is_aff_indep_dim_is_aff_gen, is_aff_indep_dim_is_aff_basis,
              dim_is_aff_indep_gen_equiv.
Proof of affine_independent_generator.

poly_Lagrange, P_approx_k:
Propagate new API (from Finite_dim).

Add and prove vectF_ms_eq, translF_ms_eq,
              barycenter_ms_eq.

Finite_dim:
Add and prove is_affine_generator_equiv.

Add and prove skip_ord_{0,max}, insert_ord_{0,max}.

Finite_family:
Make some arguments implicit.
Add and prove skipF_inj, skipF_invalF{,_rev,_equiv}.

AffineSpace:
Add and prove vectF_inj_equiv, translF_inj_equiv,
              frameF_inj_equiv, inv_frameF_inj_equiv,
              frameF_invalF{,_rev_equiv}.

Finite_dim:
Make some arguments implicit.
Add and prove span_ext, is_generator_ext, is_free_ext, is_lin_dep_ext,
              is_basis_ext, has_dim_ext, dim_ext,
              aff_span_ext, is_aff_gen_ext, is_aff_indep_ext, is_aff_dep_ext,
              is_aff_basis_ext, has_aff_dim_ext, aff_dim_ext,
              is_aff_indep_monot, is_aff_dep_monot, is_aff_indep_skipF,
              affine_independent_skipF.
Proof of affine_independent_equiv.

FE_simplex:
Remove is_free_liftF_S (use affine_independent_skipF instead).