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