Group_compl:

Add and prove f_zero_minus_opp_compat, f_opp_minus_plus_compat,
              f_plus_opp_minus_compat.

Sub_struct:
Proofs of sub{,_ms}_fun_rev.
Modify sub{,_ms}_{inj,surj,bij}_equiv.
Add and prove fct_sub_{inj,surj,bij}_{rev,equiv}.
              sub_{m,g,r,as}_fun_rev,
              {,fct_}sub_{m,g,r,as}_{inj,surj,bij}_{rev,equiv},
              {,fct_}sub_g_f_{opp,minus}_compat,
              fct_sub_ms_{inj,surj,bij}_{rev,equiv}.