proposition: Theorem surj_if_exists_right_inv f: (exists s, is_right_inverse f s) -> surjection f.
proof: Proof. move=> [s rsf]; move: (rsf) => [cp _]; move: (cp) =>[ff fs ss]. split => // y yt; exists (Vf s y). rewrite -(right_i_source rsf) in yt; rewrite ss; fprops. by rewrite (right_i_V rsf yt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)