proposition: Lemma card_max_rep_rec n m: m.+2 <= n -> card_max_rep n.+2 m.+1 = card_max_rep n.+1 m + card_max_rep n m.
proof: Proof. case: m. case:n => [|[ | [| n _]]] //; rewrite !card_max_repn0. by rewrite card_max_rep41 card_max_rep2m. rewrite card_max_repE big_hasC => //; apply /hasPn => i. rewrite mem_index_iota => /andP [la _]. have l2n3: 2 < n.+3 by rewrite !ltnS. move: (fib_smonotone_bis l2n3); rewrite (fib_pos n.+4) ltnS => lb. by rewrite (gtn_eqF (ZeckMgt2 (leq_trans lb la))). move => m lmn. set k := (fib n.+1) + (fib n.+1).-1. have kl1: (fib n.+2).-1 <= k. by rewrite - ltnS /k -addnS -!fib_pos fibSS leq_add2l fib_monotone. have kl2: k <= (fib n.+3).-1. by rewrite - ltnS /k -addnS -!fib_pos fibSS leq_add2r fib_monotone. have np:=(ltn_predK lmn). have n3: n = (n-3).+3 by rewrite - addn3 subnK // (leq_trans _ lmn). rewrite addnC !card_max_repE (big_cat_nat _ _ _ kl1 kl2) /=; congr addn. rewrite fibSS /k -[in fib n] np (fib_pos n.-1) addnS /= np big_nat_shift. apply:big_nat_cond_eq => i eq1. by rewrite n3 in eq1; move:(ZeckM_rec2 eq1); rewrite -n3 addnC => ->. rewrite fibSS /k (addnC (fib n.+2)) (fib_pos n.+1) addnS /= big_nat_shift. apply:big_nat_cond_eq => i eq1. by rewrite n3 in eq1; move:(ZeckM_rec1 eq1); rewrite -n3 addnC => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)