proposition: Lemma max_rep_fib3 n: max_rep (fib n.*2.+2) (rev (0::(succ_seq (mkseq double n)))).
proof: Proof. rewrite /max_rep. move:(max_rep_fib2 n) => /andP [sa sb]. rewrite Zeckv_rev Zeckv_cons - Zeckv_rev (eqP sb) add1n - fib_pos eqxx. by move: sa; rewrite spec_sorted_rev spec_sorted_rev andbT //;case n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)