Make K argument of plusn1 implicit.
Mv stuff around.
Rename invertible_plusn -> invertible_plusn_not_ring_charac.
Add invertible_plusn1_R, scal_ones, isobaryc_ms_eq.

Use abstract scopes in monomial too.

  {,n}eqxT{,r,c}, {insertT,skipT,replaceT}{,r,c}.
And also for associated lemmas.

                  *_distr_{l,r} -> *_plus_{r,l},
                  scalF_sum_{l,r}{l,r} -> scalF_sum_{r,l}{l,r},

       lc_kron_{l,r}_out_{l,r} -> lc_{l,r}_kron_{l,r}_out,
       baryc_kron_{l,r} -> baryc_l_kron_{l,r},
       am_ac_compat -> am_lc_compat,
       aff_gen_ms_equiv_R -> aff_gen_ms_equiv_R_lc.
Modify aff_gen_ms_equiv, aff_indep_aff_gen_R.
Add baryc_r_kron_{l,r}, am_normal,
    aff_gen_ms_equiv_R, aff_indep_aff_gen_R_lc.

               fun_ext2 and extT (with 0 or 2 arguments).
And use them!
Enjoy the new one-liner proofs... ;)

  F{T,R}0_lin_span, FR0_dual_lin_span,
  F{T,R}0_lin_gen, FR0_dual_lin_gen,
  F{T,R}0_lin_indep, F{T,R}0_dual_lin_indep,
  F{T,R}0_basis, FR0_dual_basis,
  FT0_has_dim, FR0_dual_has_dim.
Add FR0_sub_dim, FR0_sub_eq,
    FR0_dual_sub_dim, FR0_dual_sub_eq.
Modify lin_{in,}dep_1_equiv, basis_1_equiv (abstract, simpler proof).

Add le_1_n{0,1}, I_1_unit, I_1_is_unit, eqAF_1,
    F{T,R}0_dual_ext.

       lin_span_incl -> lin_span_monot_inclF,
       lin_span_monot -> lin_span_monot_invalF.
Abstract F{T,R}0_lin_span, F{T,R}0_lin_gen, F{T,R}0_lin_indep,
         F{T,R}0_basis, F{T,R}0_has_dim.
Add lin_span_incl_equiv, line_incl_equiv,
    FR0_dual_lin_span, FR0_dual_lin_gen, F{T,R}0_dual_lin_indep,
    FR0_dual_basis, FR0_dual_has_dim.

Add FT0_lin_gen, FR0_lin_gen,
    FT0_lin_indep, FR0_lin_indep,
    FT0_basis, FR0_basis, FR0_has_dim.
Proof of FT0_has_dim.
WIP: FR0_has_dim_sub.

       injF_equiv -> injF_g_equiv.
Mv {vectF,translF,frameF}_ms_eq from AffineSpace_baryc to AffineSpace_FF.
Add injF_ms_equiv.

       lin_{dep,indep}_equiv_injF -> lin_{dep,indep}_permut_equiv_injF,
       lin_{dep,indep}_equiv -> lin_{dep,indep}_permut_equiv.
Add skipF_not_inF_rev, skipF_not_inF_equiv,
    injF_equiv.

Hide section Lin_comb_Kron_R_Facts.

Simplify some proofs.
Replace *kronecker* by *kron*.

Some style unification + cosmetics.
Rename B0k_eq -> Monom_0k_eq,
       Bd0_eq -> Monom_d0_eq,
       Bd1_eq0 -> Monom_d1_eq0,
       Bd1_neq0 -> Monom_d1_neq0,
       Pdk_monotone* -> Pdk_monot*,
       am_Pd1 -> Pd1_am.

  + Finite_dim_MS_lin_map_R + Finite_dim_MS_duality + Finite_dim_AS_rest_R.
Add export modules Finite_dim_MS and Finite_dim_AS.
Update doc (used logic axioms + usage).
Update imports.