proposition: Lemma finv_eq_can : cancel f f' -> finv f =1 f'.
proof: Proof. move=> fK; have inj_f := can_inj fK. by apply: bij_can_eq fK; [apply: injF_bij | apply: finv_f]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)