proposition: Lemma max_rep_fib1 n: max_rep (fib n.*2.+1).-1 (rev (mkseq double n)).
proof: Proof. rewrite /max_rep - {2}(Zeck_fib1 n) Zeck_zeck_val eqxx andbT. rewrite spec_sorted_rev; case: n => //n /=; rewrite andbT. by elim: n (0) => // n H i /=; rewrite eqxx orbT H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)