Code review in Compl.

Tune required library files.
Add some documentation.
Move stuff around, factor arguments and compact/simplify some proofs.
Some style unification.

logic_compl:
Rename not_eq_sym_invol -> neq_sym_invol.
Add and prove iff_not_l_equiv,
              ex_EX (an alias for constructive_indefinite_description).

Subset_compl:
Use Lebesgue.Subset_dec and logic_compl instead of ClassicalEpsilon.

Function_compl:
Rename inj_comp_l -> comp_inj_l.
Add and prove fun_ext_contra{,_rev,_equiv}, surj_id, f_inv_id_{rev,equiv}.

Function_sub: WIP.

Sub_struct:
Propagate new API (from Subset_compl).