proposition: Lemma compf_rK f g : bijection g -> f \coP g -> (f \co g) \co (inverse_fun g) = f.
proof: Proof. move => bg cop. move: (composable_f_inv bg) => co1. rewrite -(compfA cop co1) (bij_right_inverse bg). by move: cop => [s1 s2 s3]; rewrite - s3 (compf_id_r s1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)