Modify def castTc.
Add and prove castT{r,c,}_comp, castT_comp_{r,c}{l,r}.

geometry:
Rename convex_envelop_cast -> convex_envelop_castF_incl (proof simplified).
Add and prove convex_envelop_castF.

FE:
Add and prove nos_eq.
Modify FE_ext (use castT).

FE_simplex:
Remove useless defs ord_nvtx_Sd, ord_nvtx_Sd.
Modify def vtx_ref, FE_cur.
Simplify proofs of K_geom_{ref,cur}_def_correct.

FE_LagP:
Simplify proof of FE_cur_eq (use castT and its properties).

Add defs castF_fun, cast2F_fun.
Add and prove castF_fun_id, cast2F_fun_id.

FE, FE_LagP:
Propagate new API (from Finite_family).

Remove useless castF_eq_sym_refl, use castF_refl/castF_id instead!
Rename castF_id -> castF_can.
Modify castF_can_{l,r}.
Add and prove castF_id.

Finite_table:
Modify castT{r,c,}_refl.
Rename castT{r,c,}}_sym -> castT{r,c,}_can.
Add and prove castT{r,c,}_id.

Sub_struct:
Rename val_inclF_compat -> in_subF (simplified),
       mk_sub_eq -> mk_sub_ext.
Add and prove mk_subF_eq, valF_eq.

Monoid*, ModuleSpace_compl, Finite_dim*, multi_index, poly_Lagrange, FE, FE_LagP :
Propagate new API (from Finite_family, Sub_struct).

Rename FF_to_list* -> to_listF*,
       FF_of_list* -> of_listF,
       FF_of_to_list* -> of_to_listF*,
       FF_to_of_list -> to_of_listF.

Monoid_compl:
Propagate new API (from Finite_family).

Add reminder.

Add and prove is_free_{sub,val}{,_rev,_equiv}.

Finite_dim_R:
Propagate new API (from Finite_dim).

Make fullset explicit in statements.
Add and prove is_generator_val{,_rev,_equiv}.
Proofs of is_finite_dim_sub_rev,
          is_finite_dim_{preimage,RgS}_val{,_rev}.

Add and prove image_preimage_val, preimage_image_val.

Finite_dim:
Add reminder.
Proofs of is_generator_sub_rev,
          image_preimage_val_ms, is_generator_preimage_val{,_rev},
          preimage_image_val_ms, is_generator_RgS_val{,_rev}.
Simplify proof of incl_RgS_val.
Add and prove is_free_has_dim_span_alt.

Fix, prove and rename KerS_m_comp -> KerS_comp.
Remove useless sections for KerS_{g,}_comp.
Fix and prove translP_orig_indep.

Add reminder.

Add reminder.

ModuleSpace_compl:
Add defs fct_scal_l, fct_scalF_l, fct_comb_lin_l.
Add and prove fct_scalF_l_eq.
Fix fct_comb_lin_l_eq.

Add reminder.

Monoid_compl:
Proof of Rbar_plus_assoc_bounded_l.
Add and prove Rbar_plus_assoc_bounded_r.

WIP: Rbar_plus_assoc_bounded_l.

filterP_rev_ord is wrong (when P is not symmetric).

Rename injS_equiv_seq -> injS_seq_equiv,
       ord0_equiv_{leq,le} -> ord0_{leq,le}_equiv,
       ord_n0_equiv_{gtn,gt} -> ord_n0_{gtn,gt}_equiv,
       ord_n0_equiv_alt -> ord_n0_nlt_equiv,
       ord0_equiv_alt -> ord0_lt_equiv,
       ord_gt_not_0 -> ord_n0_gt,
       ord_max_equiv_{geq,ge} -> ord_max_{geq,ge}_equiv,
       ord_nmax_equiv_{ltn,lt} -> ord_nmax_{ltn,lt}_equiv,
       ord_lt_not_max -> ord_nmax_lt,

Remove useless ord_not_0_gt (use ord_n0_nlt_equiv instead),
               ord_not_max_lt (use ord_nmax_lt_equiv instead),
               ord_nmax_equiv_alt (use ord_nmax_lt_equiv instead),
               ord_max_equiv_alt (use ord_max_ge_equiv + Nat.nlt_ge instead).

Finite_family, Ring_compl, poly_Lagrange:
Propagate new API (from ord_compl).

Remove useless lemmas.
Rename sub_{le,lt}_mono_r -> nat_sub_{le,lt}_mono_r,
       lt_{2,3}_dec -> ltn_{2,3}_dec,
       le_{1,2}_dec -> leq_{1,2}_dec.

ord_compl, Monoid_compl:
Propagate new API (from nat_compl).

Remove useless hypotheses.
Add doc.
Add and prove predual_basis_{in_sub,dualF,is_basis}
  (borrowed from FE.shape_fun_correct and FE.shape_fun_is_basis).

FE:
Propagate new API (from Finite_dim_R).

Remove useless inter_empty_{l,r} masking existing lemmas.
Modify and rename union_compl_{l,r} -> inter_union_compl_{l,r}.
Add and prove inter_empty_{l,r}_alt (more general),
              diff_compl_{l,r}_diag,
              sym_diff_empty_{l,r}_rev, sym_diff_eq_{l,r}.

Add and prove pair_correct, pair_sym, pair_in_{l,r}{,_alt},
              inter_singleton_{l,r}_{in,out},
              union_{left,right}{,_rev_equiv}, union_compl_{l,r},
              inter_union_inj_{l,r}{_incl,}.

Add and prove not_iff_equiv.

Subset_compl:
Add and prove same_refl, subset_ext_contra{,_rev_equiv}.
Proof of inter_eq_union_incl.

WIP: inter_eq_union_incl.

Rename is_generator_fullset_compat_gen -> is_generator_sub,
       is_generator_fullset_compat -> is_generator_sub_alt,
       is_finite_dim_fullset_compat_gen -> is_finite_dim_sub,
       is_finite_dim_fullset_compat -> is_finite_dim_sub_alt.
Add and prove {is_generator,is_finite_dim}_sub_equiv, incl_RgS_val,
              is_finite_dim_{preimage,RgS}_val_equiv.
WIP: {is_generator,is_finite_dim}_sub_rev,
     {is_generator,is_finite_dim}_{preimage,RgS}_val{,_rev}.

Finite_dim_R:
WIP: proof of has_dim_le_eq using has_dim_le_eq_alt.

Use f_{opp,minus}_compat.

AffineSpace:
Add defs f_{vectF,translF}_compat{_gen,}.
To do: add properties.

Sub_struct:
Move stuff around.
Modify val_{zero,plus,sum,opp,minus,one,mult,scal,comb_lin,{vect,transl}{,F}}.
Add and prove span_{struct,m,g,r,ms,as}_full,
              val_morphism_{m,g,r}, val_{lin,aff}_map,
              {RgS,preimage}_val_{m,g,ms,as}_eq,
              {preimage,RgS}_val_compatible_{m,g,ms}{,_rev,_equiv}.
WIP: {preimage,RgS}_val_compatible_as{,_rev,_equiv}.

Hide stuff about dual/bidual/predual_basis.
Say that defining shape_fun as the predual basis of Sigma would need significant additional developments.

Rename bidual_nat_isom* -> bidual_isom*.

Add def pt_eval.

Monoid_compl, ModuleSpace_compl:
Rename *_pt_value -> *_pt_eval.

Finite_dim, FE_simplex:
Propagate new API (from ModuleSpace_compl).

Finite_dim:
Proofs of bidual_pt_eval, bidual_nat_isom_correct.

Make some arguments implicit.

Finite_dim_R:
Add many local definitions to ease reading.
Make some arguments implicit.
Rename dual_is_linear_mapping -> dual_lin_map.
Add def bidual_basis, bidual, bidual_nat_isom, predual_basis.
Add and prove dual_has_dim, dual_lin_map_{rev,equiv}.
WIP: bidual_pt_eval, bidual_nat_isom_{correct,lin_map,inj,bij},
     predual_basis_{dualF,is_basis,correct}.

Add and prove {row1T,col1T}_correct.

ModuleSpace_R_compl:
Add and prove comb_lin2_alt'.

matrix:
Add notation for mx_one.
add and prove mx_one_sym.

Finite_dim:
Remove useless span_ext, aff_span_ext.
Rename span_eq -> span_ext.
Add and prove aff_span_ext.

Finite_dim_R:
Add defs dual, bidual_basis.
Add and prove dual_basis_decomp_compat, dual_basis_decomp,
              dual_is_linear_mapping, dual_uniq, dual_is_finite_dim.
WIP: transition_matrix_ex, properties of bidual_basis, predual_basis (def).

P_approx_k:
Propagate new API (from Finite_dim).

Some cleaning/compacting about duality.
Rename is_dual_family -> dualF,
       is_dual_is_free -> dualF_is_free,
       is_dual_is_free_rev -> dualF_is_free_rev,
       is_dual_is_basis -> dualF_is_basis_equiv.
Remove first definition of dual_basis (total fun on E),
  keep the second (on sub_ms HPE).
Rename dual_basis2 -> dual_basis,
       dual_basis2_is_linear_mapping -> dual_basis_lin_map,
       dual_basis2_kronecker -> dual_basis_dualF,
       dual_basis_is_basis2 -> dual_basis_is_basis.
TODO: predual_basis.

FE:
Propagate new API (from Finite_dim_R).

Add and prove {,is_}unit_type_correct.

Function_compl:
Add and prove fun_to_is_unit_is_unit, fun_from_empty_is_unit.
Rename fun_to_singl_is_singl -> fun_to_unit_unit,
       fun_from_empty_is_singl -> fun_from_empty_unit.

Finite_family:
Rename hat0F_singl -> hat0F_unit.
Add and prove hat0F_is_unit.

Finite_table:
Rename hat0nT_singl -> hat0nT_unit,
       hatm0T_singl -> hatm0T_unit.
Add and prove hat0nT_is_unit, hatm0T_is_unit.

Monoid_compl, Finite_dim, multi_index:
Propagate new API (from Finite_family).

  from ModuleSpace_compl into ModuleSpace_R_compl,
  from Finite_dim into Finite_dim_R.