proposition: Lemma max_rep_fib4 n: max_rep (fib n.*2.+3) (rev (1:: (map double (iota 1 n)))).
proof: Proof. rewrite /max_rep. move:(max_rep_fib1 n.+1) => /andP; rewrite /mkseq /=. set s := [seq i.*2 | i <- iota 1 n]; move => [sa /eqP]. rewrite !Zeckv_rev !Zeckv_cons doubleS add1n add2n => ->. by move: sa; rewrite !spec_sorted_rev /s- fib_pos eqxx /= !andbT; case n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)