proposition: Lemma inj_if_exists_left_invC (a b:Set) (f:a-> b): (exists r, is_left_inverseC f r) -> injectiveC f.
proof: Proof. move=> [r ilr] x x'. by move /(congr1 r); move: (ilr x) (ilr x') => /= -> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)