Rm wrong doc.

       inj_ASdki_incr -> inj_ASdki_monot.
Compact/simplify proofs.

Add gr*lex_lt_insertF, gr*lex_lt_mul.

Hide unused.

Modify insert_f_ord, insert_f_ord_correct_{l,r} (param in front).
Add insert_f_ord_inj,
    insertF_permutF, revF_insertF, *lex_insertF,
    nat_mul_plus_{l,r}, sum_mult, sum_def_nat_contra,
    gr*lex_insertF, gr*lex_lt_zl.
WIP: insertF_revF.
Keep initial version of lex_insertF.
Rm grsymlex_br_plus_compat_l.

Factor hypotheses.

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.