Rm useless node_ref_eqF, node_ref_CSdk, node_ref_ASdki,
           node_d0_eq, sub_vtxF, sub_vtx_refF, sub_nodeF.

       sub_nodeF_alt -> sub_nodeF.
Rm useless sub_node_ref_eq, T_geom_sub_nodeF.
The proof of sub_node_out_Hface_0 is now based on sub_node_ref_out_Hface_ref_0.

Add sub_node_ref, sub_node_ref_eq, sub_node_ref_out_Hface_ref_0, nodeF.
Rename sub_nodeF -> sub_nodeF_alt,
       sub_node_ref -> sub_node_ref_sub_node.
Modify sub_node.
WIP: sub_nodeF, sub_node_out_Hface_0 (should use sub_node_ref_out_Hface_ref_0).
Hide presumably useless
  sub_nodeF_alt, sub_node_ref_sub_node, sub_node_ref_eq, T_geom_sub_nodeF.

Add vtx_ref_sum,
    node_ref_d0, node_ref_d0_eqF, node_d0_eq, node_ref_d0_node.
Modify node_d0.
Rm useless T_geom_node.

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.

# Conflicts:
#	FEM/FE_LagP.v

# Conflicts:
#	FEM/FE_LagP.v

Add unisolvence_inj_Hface (candidate to factor step 1 and face unisolvence).

Modify node_ref_CSdk, node_ref_ASdki.
Add T_geom_inj_l, T_geom_comm.
WIP: T_geom_sym.

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}.