proposition: Lemma compf_lK' f g: bijection g -> function f -> target g = target f -> g \co (inverse_fun g \co f) = f.
proof: Proof. move => bg ff tf. move:(inverse_bij_fb bg) => ibg. move: (ifun_involutive (proj1 (proj1 bg))) => ffi. rewrite -{1} ffi; apply: (compf_lK ibg); saw; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)