proposition: Lemma sorted_ggenW s : sorted ggen s -> sorted gtn s.
proof: Proof. by case: s => //= n s; elim: s n => //= m s IHs n /andP [/ltnW -> /IHs]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)