proposition: Lemma section_unique f: {when (is_right_inverse f) &, injective Imf }.
proof: Proof. move=> s s' rsf rs'f rg. move: (proj32_1 rsf)(proj32_1 rs'f) => fs fs'. move: (right_i_source rsf) (right_i_source rs'f) => ss ss'. apply: function_exten =>//. by rewrite (right_i_source rsf). by rewrite (right_i_target rsf) (right_i_target rs'f). move=> x xs. move: (Imf_i fs xs). move: xs;rewrite rg ss => xs /(Imf_P fs') [y]; rewrite ss' => ys ww. move: (f_equal (fun z => Vf f z) ww). by rewrite(right_i_V rs'f ys) (right_i_V rsf xs) ww => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)