proposition: Lemma Zeck_ggen n: sorted ggen (Zeck n).
proof: Proof. elim: n {-2} n (leqnn n) => [ [] | n Hr k] //;rewrite leq_eqVlt ltnS. case /orP => //; [move/eqP => -> | by apply: Hr]. move: (fib_content_lt n)(fib_content_large n); rewrite Zeck_S' /= => sa sb. move:(Hr _ sb) sa; case: (_ - _) => // v; rewrite Zeck_S' /= => -> la. move/andP: (fib_contentP v) => [lb _]; move: (leq_ltn_trans lb la). by move/fib_monotone_bis; rewrite ltnS andbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)