proposition: Theorem inj_if_exists_left_inv f: (exists r, is_left_inverse f r) -> injection f.
proof: Proof. move=> [r lrf]; split; first by move: lrf => [ cp _ ]; fct_tac. move=> x y xs ys sv. by rewrite - (left_i_V lrf xs) - (left_i_V lrf ys) sv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)