Add and prove succF_correct.

binomial_compl:
Moved from Compl to Algebra.
Add and prove binom_sym_alt, binom_rising_sum_{l,r},
              pbinomS_pascal, pbinomS_rising_sum_{l,r}.

Ie, replace the inhabited axiom of affine space by the witness inhabitant.

Add binomial_compl (for pbinom from mathcomp).

Mv {nat,ord}_compl, Finite_{family,table} from Algebra to Compl.
Smooth imports.

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