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