Modify nat_ind2_strong.

Solve last admitted.

When two functions are stated to be inverse, name it <fun>_can_{l,r}.

Signed-off-by: Houda Mouhcine <houda.mouhcine@inria.fr>

Rename LInt_SFp -> LInt_SF,
       *SFp_* -> *SF_* (when there is no nonneg hypothesis),
       SF_* -> SFplus_* (when there is a nonneg hypothesis),
       Lint_SFp_eq_other_list -> Lint_SFp_skip_0.

       aff_dim -> has_aff_dim,
  except when the lemma actually state something on the dimension,
  eg dim_is_unique.
Rename *_finite_dim_* -> *_fin_dim_*.

Compact proof of lm_decomp.

Simplify proof of fct_lc_r_lm_alt.
Rename component_sum_lm -> lm_component_sum.
Compact proof of am_Pd1.

Simplify proof of itemF_kronecker_eq.

Add fct_{inv,div}_eq, fct_scal_eq, lm_fct_scal.
Proofs of lm_fct_{zero,sum,opp,minus},
Rename fct_scal_l_lm -> lm_fct_scal_l,
       fct_scal_r_lm -> lm_fct_scal_r

    f_{plus,zero}_compat_mapF, morphism_m_{mapF,map2F},
    f_{opp,minus}_compat_mapF, morphism_g_{mapF,map2F},
    f_{mult,one}_compat_mapF, morphism_r_{mapF,map2F},
    lm_sum, lm_fct_plus,
    f_scal_compat_mapF, lm_{mapF,map2F}.
Rename lm_f_scal_l -> fct_scal_l_lm,
       lc_lm_compat_l -> fct_lc_l_lm,
       lm_f_scal_r -> fct_scal_r_lm,
       lc_lm_compat_r* -> fct_lc_r_lm*,
       lc_fun_lc -> f_lc_compat_lms.
WIP: lm_fct_{zero,sum,opp,minus,scal}, fct_scalF_l_lm.