So long Rlists!

Bi_fun, Bint_Bif, :
Use rewrite/apply from SSReflect.

Add AbelianMonoid stage in the hierarchy.
Use rewrite/apply from SSReflect when necessary.

check_sub_structure:
Obsolete, use FEM/Linalg/Sub_struct.

(Need to define the inverse of Ak_d applied to itemF).

Define node_Pk_d_cur with barycentric.

Add nat2_ind_alt_11 lemma.
Use double induction in the unisolvence proof.

AffineSpace:
Add and prove vect_transl_assoc.
Add defs f_{vect,transl}_compat_gen.
Add and prove f_vect_transl_compat_gen_equiv,
              f_plus_{transl,vect}_compat{,_equiv},
              f_{transl,vect}_compat_gen_flm_uniq,
              is_affine_mapping_flm_orig_indep.
Rename is_affine_mapping_{vect,transl}_compat -> is_affine_mapping_{vect,transl}.

Sub_struct:
Make some arguments implicit.
Rename {vect,transl}_closed* -> {vect,transl}_closed_gen*,
       compatible_as_sub_ms_orig_indep -> compatible_as_sms_orig_indep.
Add defs {vect,transl}_closed.
Add and prove vect_transl_closed_equiv.
WIP: {vect,transl}_closed_orig_indep.

Add def sumK_closed.
Add and prove plus_zero_sumK_closed, sumK_plus_zero_closed, sumK_plus_zero_closed_equiv,
              compatible_r_sumK, span_r_sumK.
Remove useless defs vect_closed, transl_closed.
Rename {vect,transl}_closed_gen* -> {vect,transl}_closed*.
Add and prove compatible_ms_{transl,vect}, compatible_ms_as,
              compatible_as_plus (extracted),
              compatible_as_ms, compatible_as_equiv.
Section Sub_AffineSpace_Def:
  modify HK, HPE0 -> O+HO, PV.

Add and prove iff_sym_equiv.

Ring_compl:
Add def two, and notation 2.

ModuleSpace_compl:
Add lemmas with 2 + use plusn1.

AffineSpace:
Use plusn1 and 2.
Add and prove parallelogram_transl_vect.
Simplify proof of transl_vect_barycenter.

Finite_dim:
Rename non_zero* -> nonzero*.

WIP: f_{vect,transl}_compat_flm_uniq.

Sub_struct:
Move stuff around.
Add and prove vect_transl_closed_gen_equiv, vect_transl_closed_equiv.
Rename sub_ms_orig_compat_vect -> sub_ms_orig_indep_vect,
       sub_ms_orig_compat_transl -> sub_ms_orig_indep_transl,
       vect_closed_orig_compat -> vect_closed_orig_indep,
       transl_closed_orig_compat -> transl_closed_orig_indep.
WIP: vect_closed_sms_uniq, vect_closed_compatible_as.

Rename is_affine_mapping_comb_lin_compat -> is_affine_mapping_comb_aff_compat.

poly_Lagrange:
Propagate new API (from AffineSpace).

Add and prove is_affine_mapping_ext.

Sub_struct:
Add and prove compatible_ms_plus_equiv.
WIP on sub-affine spaces: replace inductives by direct defs on sub_ms.
Temporarily hide what is not compiling...

poly_Lagrange, FE_simplex:
Propagate new API (from AffineSpace).

Add and prove inter_empty_{l,r}.

ModuleSpace_compl:
Add and prove f_plus_scal_compat_is_linear_mapping,
              is_linear_mapping_compose.

AffineSpace:
Proofs of vectF_{singleF,coupleF,tripleF}.
Rename f_barycenter_compat -> is_affine_mapping,
       is_affine_mapping_ms_alt -> is_linear_affine_mapping_ms,
       is_affine_mapping_ms_is_linear_mapping -> is_affine_linear_mapping_ms.
Add and prove f_vect_transl_compat_equiv, f_{vect,transl}_plus_compat,
              is_affine_mapping_{vect,transl}_compat,
              is_affine_mapping_is_bij_equiv,
              fct_lm_compose, is_affine_compose,
              fct_lm_ms_eq, fct_lm_ms_eq_ex.
Modify and prove f_{vect,transl}_compat_orig_indep.
Remove old defs f_{vect,transl}_compat', is_affine_mapping_{v,t}
                and associated lemmas.

Define the face hyperplane.

Define Ck_d.

Proofs about FF_to/of_list
Proof of concatnF_correct1!

Add and prove nat2_ind_alt{_1l,_1r,_00,}.

Sub_struct:
Hint.

Add and prove is_linear_mapping_comb_lin,
              dot_product_insertF, sumK_insertF,
              alt_ones_3_eq, sumK_alt_ones_3.
Add def unit_partition.
Add and prove unit_partition_correct_{0,S}, sumK_unit_partition,
              unit_partition_1_eq, sumK_unit_partition_1,
              sumK_unit_partition_1_invertible.

AffineSpace:
Tune precedence of notations (to force use of parentheses for better readability).
Modify notation for transl ++ -> +++.
Add and prove vect_transl_plus, vect_transl_scal.
Modify defs vectF, translF (use mapF).
WIP: vectF_{singleF,coupleF,tripleF}.
Add and prove vectF_mapF, translF_mapF,
              barycenter_correct_orig_equiv,
              transl_vect_barycenter{,_alt}, transl_plus_barycenter{,_alt},
              transl_scal_barycenter.
Rename is_affine_mapping -> f_barycenter_compat,
       f_vect_compat -> f_vect_compat',
       f_transl_compat -> f_transl_compat',
       is_affine_mapping_equiv -> is_affine_mapping_equiv'.
Add def fct_lm, f_vect_compat, f_transl_compat, is_affine_mapping.
Add and prove fct_lm_orig_indep,
              f_vect_compat_orig_indep, f_transl_compat_orig_indep,
              is_affine_mapping_equiv.
WIP: revise properties of is_affine_mapping (to get rid of primes).

Sub_struct:
Propagate new API (from AffineSpace).