proposition: Lemma right_inverse_fi f s: is_right_inverse f s -> injection s.
proof: Proof. move=> lrf; apply: inj_if_exists_left_inv. by exists f; apply: left_inverse_from_right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)