Try to unify is_affine_mapping and compatible_as.

AffineSpace:
Add and prove vect_transl_assoc.
Add defs f_{vect,transl}_compat_gen.
Add and prove f_vect_transl_compat_gen_equiv,
              f_plus_{transl,vect}_compat{,_equiv},
              f_{transl,vect}_compat_gen_flm_uniq,
              is_affine_mapping_flm_orig_indep.
Rename is_affine_mapping_{vect,transl}_compat -> is_affine_mapping_{vect,transl}.

Sub_struct:
Make some arguments implicit.
Rename {vect,transl}_closed* -> {vect,transl}_closed_gen*,
       compatible_as_sub_ms_orig_indep -> compatible_as_sms_orig_indep.
Add defs {vect,transl}_closed.
Add and prove vect_transl_closed_equiv.
WIP: {vect,transl}_closed_orig_indep.