Modify nat_ind2_strong.

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.

Comment unused admitted results (and rename dmit -> glop).

Subset_system:
Add and prove Gen_Prod_Gen_Product.

- Ajout des fichiers Makefile et _CoqProject à la racine.
- Suppression des Makefile et _CoqProject des sous-répertoires.
- Ajout des dépendances dans le README.md
- Ajout de spécificateurs 'From ... Require' pour lever les ambigüités
  en cas de différents R_compl ou logic_compl
- renommage de measurable_fun-new.v en measurable_fun_new.v

So long Rlists!

Bi_fun, Bint_Bif, :
Use rewrite/apply from SSReflect.

Create a new file of bijectivity with all necessary lemmas.

New version of ae_op_compat is now proved using the previous result.

(includes bochner)

Function stuff moved to Function.v.
Some renaming.

(Some are still embryonic)

measurable_fun_swap.

Prove correctness results.