proposition: Lemma compf_regr f f' g : bijection g -> g \coP f -> g \coP f' -> g \co f = g \co f' -> f = f'.
proof: Proof. move => bg pa pb pc. by rewrite - (compf_lK bg pa) - (compf_lK bg pb) pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)