fact: Definition strip (X: seq (A*A*B)) : seq (A*B) := map (fun (ab:A*A*B) => let (aa,b) := ab in let (a,_) := aa in (a,b)) X.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)