proposition: Lemma mapK_in (A : {pred S}) (f : S -> T) (g : T -> S) : {in A, cancel f g} -> {in [pred s | all [in A] s], cancel (map f) (map g)}.
proof: Proof. by move=> fK; elim=> //= x s IHs /andP[/fK-> /IHs->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)