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.

  and move it to Finite_dim.lmS_bijS_sub_gather_equiv.

FE:
Add def nvtx_of_shape.

FE_LagP:
Propagate new API (from Finite_dim).

Add and prove not_in_empty{set,}, in_full{set,}.

Finite_dim:
Add and prove lmS_{injS,bijS}_sub_dim_equiv, lmS_bijS_sub_full_equiv.

FE, FE_simplex:
Remove obsolete sigma_injS_equiv, bijS_equiv_sub_ms
  (use new lmS_bijS_sub_full_equiv instead).

Rename sub_Ker_equiv -> Ker_sub_KerS_equiv,
       KerS_sub_equiv -> KerS_Ker_sub_equiv,
       sub_Rg_equiv -> Rg_sub_RgS_equiv,
       RgS_sub_equiv, RgS_Rg_sub_equiv.
Add and prove Ker_sub_zero_equiv,
              mk_sub_g_zero{,_equiv}, mk_sub_g_inj,
              Ker_sub_g_KerS_zero_equiv,
              KerS_g_zero_equiv_alt, Ker_sub_g_zero_equiv,
              gmS_injS_sub_equiv_alt, gmS_bijS_sub_equiv{,_alt},
              Ker_fct_sub_g_KerS_zero_equiv, Ker_fct_sub_g_zero_equiv,
              gmS_bijS_fct_sub_equiv,
              mk_sub_r_inj, mk_sub_ms_inj,
              Ker_sub_ms_KerS_zero_equiv,
              KerS_ms_zero_equiv_alt, Ker_sub_ms_zero_equiv,
              lmS_injS_sub_equiv_alt, lmS_bijS_sub_equiv{,_alt},
              Ker_fct_sub_ms_KerS_zero_equiv, Ker_fct_sub_ms_zero_equiv,
              lmS_bijS_fct_sub_equiv.

              sub_m_f_sum_compat, gmS_injS_sub_equiv,
              sub_{Ker,Rg}_equiv, {KerS,RgS}_sub_equiv,
              fct_sub_m_f_sum_compat, gmS_injS_fct_sub_equiv,
              sub_ms_f_comb_lin_compat, lmS_injS_sub_equiv,
              fct_sub_ms_f_comb_lin_compat, lmS_injS_fct_sub_equiv.

Add and prove f_zero_minus_opp_compat, f_opp_minus_plus_compat,
              f_plus_opp_minus_compat.

Sub_struct:
Proofs of sub{,_ms}_fun_rev.
Modify sub{,_ms}_{inj,surj,bij}_equiv.
Add and prove fct_sub_{inj,surj,bij}_{rev,equiv}.
              sub_{m,g,r,as}_fun_rev,
              {,fct_}sub_{m,g,r,as}_{inj,surj,bij}_{rev,equiv},
              {,fct_}sub_g_f_{opp,minus}_compat,
              fct_sub_ms_{inj,surj,bij}_{rev,equiv}.

Add alias classic_dec for excluded_middle_informative.

Finite_family, Finite_table, Monoid_compl, Ring_compl, AffineSpace,
  Sub_struct, Finite_dim, multi_index, FE:
Propagate new API (from logic_compl).

Make some arguments explicit.
Add and prove sub_{inj,surj,bij}_{rev,equiv},
              sub_ms_{inj,surj,bij}_{rev,equiv}.
WIP: sub_fun_rev, sub_ms_fun_rev.

P_approx_k:
Remove useless (use replace2F_equiv_def instead of replaceF_switch).

Add some doc.

Rename f_inv_correct_{l,r} -> f_inv_can_{l,r}.

Function_sub:
Add def involS.
Add and prove involS_injS, involS_bijS.
Rename f_invS_canS_l <-> f_invS_canS_r.
Add and prove f_invS_uniq_{l,r}, f_invS_{bijS,injS,surjS},
              f_invS_eq_equiv, f_invS_neq_equiv,
              f_invS_ext, f_invS_invol{,_alt},
              f_invS_id{,_rev,_equiv}.

ord_compl, Finite_family, ModuleSpace_compl, AffineSpace, Finite_dim,
  poly_Lagrange, P_approx_k, FE_LagP:
Propagate new API (from Function_compl).

FE_LagP:
Propagate new API (from Function_sub).

Shorten some proofs.
Add and prove f_inv_id_{l,r}.

Generalize funS_id.
Add and prove canS_id_{l,r}, bijS_id.

MonoidComp:
Propagate new APi (from Function_sub).

Add and prove bij_ex_uniq{,_rev}.
Simplify proof of bij_ex_uniq_equiv.

AffineSpace:
Simplify proofs using bij_ex_uniq_equiv.

Add and prove can_ext{_l,_r,},
              bij_ext, bij_comp_compat, bij_can_uniq_{l,r}.

AffineSpace:
Propagate new APi (from Function_compl).

Move stuff around.
Add and prove Rg_ext, surj_ext, surj_comp_{compat,reg}.

Function_sub:
Add and prove surjS_id, surjS_has_right_inv.

Add and prove inj_ext, inj_comp_{compat,reg}, inj_can_uniq_l.

ord_compl:
Propagate new API (from Function_compl).

Rename cancel_id -> can_equiv.
Add and prove comp_id, can_id.

Add and prove imp_not_{l,r}_{and,or}_equiv,
              not_imp_not_{l,r}_{and,or}_equiv.

Function_compl:
Add and prove surj_can_uniq_r, inj_contra_{rev,equiv}.

Function_sub:
Add and prove imS_dec,
              injS_id, injS_contra{,_rev,_equiv}, injS_equiv,
              injS_canS_uniq_l, comp_injS_r, surjS_canS_uniq_r,
              injS_has_left_inv.

Remove useless lemmas.

Function_sub:
Make some arguments implicit, others explicit.
Add def same_funS.
Add and prove same_funS_{refl,sym,trans},
              RgS{,_gen}_ext, funS_ext, injS_ext,
              surjS_ext, surjS_RgS_equiv,
              canS_ext{_l,_r,}, canS_{injS,surjS}, injS_canS_sym,
              bijS_ext, bijS_RgS, bijS_canS_uniq_{l,r},
              bijS_canS_sym, bijS_canS_bijS.
Rename surjS_equiv -> surjS_RgS_gen_equiv,
       surjS_equiv_alt -> surjS_RgS_equiv_alt.

Finite_family, MonoidComp, Sub_struct, Finite_dim:
Propagate new API (from Function_sub).

sym_eq, Logic.eq_sym -> eq_sym.

Add prop_ext/proof_irrel, aliases for propositional_extensionality/proof_irrelevance.

Function_compl:
Rename bij_ex_uniq -> bij_ex_uniq_equiv.

Function_sub:
Add doc.
Move stuff around.
Modify def bijS.
Rename bijS_alt -> bijS_spec,
       bijS_ex -> bijS_ex_uniq_equiv (modified).
Rm double funS_comp.
Add and prove inj_S_equiv.

ord_compl, Finite_family, MonoidComp, AffineSpace, Sub_struct, Finite_dim,
  multi_index, poly_Lagrange, FE, FE_simplex, FE_LagP:
Propagate new API (from logic_compl, Function_compl, Function_sub).

ord_compl:
Make some arguments implicit.

{Monoid,Group,Ring,ModuleSpace}_compl, AffineSpace:
Add and prove inhabited_fct_{m,g,r,ms,as}.