proposition: Lemma perm_eq_image : {subset (image f P) <= (image g P)} -> perm_eq (image f P) (image g P).
proof: Proof. move=> imfsubimg. rewrite uniq_perm // ?uniq_image //. have []:= (uniq_min_size (uniq_image Hf) imfsubimg)=> //. by rewrite !size_map. Qed.
imports: mathcomp(all_ssreflect all_algebra)