proposition: Lemma card_max_repn2n n: card_max_rep n.+2 n = 1.
proof: Proof. move: (fib_ge2_alt n); set p := (fib n.+3).-2 => pv. have la: (fib n.+2).-1 <= p by rewrite - 2!ltnS -pv -fib_pos fib_smonotone_bis. have lb: p <= (fib n.+3).-1 by rewrite pv /=. rewrite card_max_repE (big_cat_nat _ _ _ la lb) pv /= big_hasC. by rewrite big_ltn_cond // /p ZeckM_fibm2 size_rev size_iota eqxx big_geq. apply/hasPn => i; rewrite mem_index_iota /p. case:(posnP n)=> [ | /prednK nv]; first by move ->; rewrite ltn0 andbF. rewrite ltn_neqAle (andbC (i != _)) andbA -(ltnS i) -/p -[p.+1]/(p.+2.-1) -pv. rewrite -nv => /andP [] /ZeckM_bound3 /leqifP; rewrite nv; case:eqP => //. by move => _ /ltn_eqF ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)