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