proposition: Lemma section_uniqueC (a b:Set) (f:a->b)(s:b->a)(s':b->a): is_right_inverseC f s -> is_right_inverseC f s' -> (forall x:a, (exists u:b, x = s u) = (exists u':b, x = s' u')) -> s =1 s'.
proof: Proof. move=> r1 r2 sp x. have [u' eql]: (exists u' : b, s x = s' u') by rewrite- (sp (s x)); exists x. move: (f_equal f eql); rewrite (right_i_v x r1) (right_i_v u' r2). by rewrite eql; move=>->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)