feat(data/list/perm): subperm_ext_iff (#8504)
feat(data/list/perm): subperm_ext_iff (#8504)

A helper lemma to construct proofs of `l <+~ l'`. On the way to proving
`l ~ l' -> l.permutations ~ l'.permutations`.





leanprover-community/mathlib,leanprover-community/mathlib