Use unique_choice instead of choice when possible (Function_compl,
  AffineSpace, Finite_dim_R).

Function_compl:
Rename and move f_inv_EX -> bij_EX.
Add and prove bij_ex.
Extract inj_surj_ex_uniq{,_rev} from bij_ex_uniq{,_rev}.
Simplify proofs of bij_equiv, bij_ex_uniq{,_rev}.

Simplify proofs in geometry.
Tune imports in FEM.

No need for Classical (it is exported in ClassicalEpsilon).
Doc.

WIP: tune imports.

cated files.

Move shape_fun_ext to FE.

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