Rename filterPF_eq_funF -> filterPF_eq.
Rm useless results.

Mv stuff around.

Use abstract scopes in monomial too.

Generalize {filter0F,filter_n0F}_correct into filter_{,n}eqF_correct.
Rm now useless specific results.

Rm now useless specific results.

Generalize insert0F_Rg into insertF_Rg.
Add mapF_replace0F.

  itemF, insert0F, replace0F, squeezeF.
And also for associated lemmas.

Rename insertF_inj_l <-> insertF_inj_r,
       insertF_nextF_compat_l <-> insertF_nextF_compat_r,
       insert2F_inj_l -> insert2F_inj_r,
       insert2F_inj_r{0,1} -> insert2F_inj_l{0,1},
       insert2F_nextF_compat_l -> insert2F_nextF_compat_r,
       insert2F_nextF_compat_r{0,1} -> insert2F_nextF_compat_l{0,1},
       replaceF_reg_l <-> replaceF_reg_r,
       replaceF_neqxF_compat_l <-> replaceF_neqxF_compat_r,
       replace2F_reg_l -> replace2F_reg_r,
       replace2F_reg_r{0,1} -> replace2F_reg_l{0,1},
       insertT{r,c,}_inj_l <-> insertT{r,c,}_inj_r,
       insertT{r,c,}_nextT_compat_l <-> insertT{r,c,}_nextT_compat_r,
       replaceT{r,c,}_reg_l <-> replaceT{r,c,}_reg_r,
       replaceT{r,c,}_neqxT{r,c,}_compat_l <-> replaceT{r,c,}_neqxT{r,c,}_compat_r,
       {insertF,replaceF}_zero_reg_l <-> {insertF,replaceF}_zero_reg_r,
       {insert2F,replace2F}_zero_reg_l -> {insert2F,replace2F}_zero_reg_r,
       {insert2F,replace2F}_zero_reg_r{0,1} -> {insert2F,replace2F}_zero_reg_l{0,1},
       {insertT,replaceT}{r,c,}_zero_reg_l <-> {insertT,replaceT}{r,c,}_zero_reg_r,

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

  {,n}eqx{,2}F, unfunF/maskPF, insert{,2}F/skip{,2}F/replace{,2}F,
  filter_{,n}eqF{_gen,}, splitF_eqF{_gen,}.
And also for some lemmas.
Add notations {insertF,skipF,replaceF}{0,max}, {,n}eqxF{0,max}.

       or_distr_{l,r} -> or_and_{l,r}.

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

Proof of aff_indep_decomp_uniq_rev.

                   lin_basis_aff_basis{,_rev,_equiv}.

    lin_indep_aff_indep{,_rev,_equiv}.

Add sum_skipF_compat, sum_eqxF_reg, sum_skipF_reg.

    fct_lm_gather_ms, am_gather{_equiv,,_rev}_ms (proofs redone, why?)

Rename lm_scatter <-> lm_scatter_rev.

Rename am_scatter <-> am_scatter_rev.

Proof of insertF_am.

Add LagPd1_ref_kron_vtx, LagPd1_ref_vtx_skipF.
Proof of Hface_ref_is_Ker.