proposition: Lemma left_inverse_comp_id (a b:Set) (f:a->b) (H:inhabited a): injectiveC f -> (left_inverseC f H) \o f =1 @id a.
proof: Proof. move => fi t; apply fi; rewrite composeC_ev;apply: left_inverseC_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)