proposition: Lemma left_inverse_fs f r: is_left_inverse f r -> surjection r.
proof: Proof. move=> lrf; apply: surj_if_exists_right_inv. by exists f; apply: right_inverse_from_left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)