Make some arguments implicit.

Rename sub_Ker_equiv -> Ker_sub_KerS_equiv,
       KerS_sub_equiv -> KerS_Ker_sub_equiv,
       sub_Rg_equiv -> Rg_sub_RgS_equiv,
       RgS_sub_equiv, RgS_Rg_sub_equiv.
Add and prove Ker_sub_zero_equiv,
              mk_sub_g_zero{,_equiv}, mk_sub_g_inj,
              Ker_sub_g_KerS_zero_equiv,
              KerS_g_zero_equiv_alt, Ker_sub_g_zero_equiv,
              gmS_injS_sub_equiv_alt, gmS_bijS_sub_equiv{,_alt},
              Ker_fct_sub_g_KerS_zero_equiv, Ker_fct_sub_g_zero_equiv,
              gmS_bijS_fct_sub_equiv,
              mk_sub_r_inj, mk_sub_ms_inj,
              Ker_sub_ms_KerS_zero_equiv,
              KerS_ms_zero_equiv_alt, Ker_sub_ms_zero_equiv,
              lmS_injS_sub_equiv_alt, lmS_bijS_sub_equiv{,_alt},
              Ker_fct_sub_ms_KerS_zero_equiv, Ker_fct_sub_ms_zero_equiv,
              lmS_bijS_fct_sub_equiv.