Generalize aff_gen_ms_equiv into aff_gen_equiv,
           aff_indep_aff_gen_R into aff_indep_aff_gen_full.

Temporarily admit what do not come naturally.

Factor baryc_bc_aux, fix proofs of baryc_bc_sum and baryc_bc_baryc.

Add fct_AS_MSAS_mixin, fct_AS_MSAS,
    MSAS_fct_MS_mixin, MSAS_fct_MS.

Stuff about comp_l/comp_r.

  MS_R_compl.part1F_fct_lm -> MS_lin_map.part1F_lm,
  part1F_am.
Generalize pt_eval_am, component_am, constF_am, skipF_am to affine spaces.
Add part1F_fct_lm.

    coercions {,Abs}Ring_{Module,Affine}Space.

Is it provable?
And btw, how to use it?

Maj R_AffineSpace (still commented).