proposition: Lemma compf_lK f g : bijection g -> g \coP f -> (inverse_fun g) \co (g \co f) = f.
proof: Proof. move => bg cop. have co1 := (composable_inv_f bg). rewrite (compfA co1 cop) (bij_left_inverse bg). by move: cop => [s1 s2 ->]; rewrite (compf_id_l s2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)