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