Add and prove val_zero_equiv, mk_sub_zero,

              sub_m_f_sum_compat, gmS_injS_sub_equiv,
              sub_{Ker,Rg}_equiv, {KerS,RgS}_sub_equiv,
              fct_sub_m_f_sum_compat, gmS_injS_fct_sub_equiv,
              sub_ms_f_comb_lin_compat, lmS_injS_sub_equiv,
              fct_sub_ms_f_comb_lin_compat, lmS_injS_fct_sub_equiv.