proposition: Lemma card_min_rep_rec n m: card_min_rep n.+2 m.+1 = card_min_rep n.+1 m.+1 + card_min_rep n m.
proof: Proof. case: (posnP n) => np. by rewrite np card_min_rep1m card_min_rep0m card_min_rep2m eqSS. set k := fib n.+2 + fib n. have kl1: (fib n.+2) <= k by rewrite leq_addr. have kl2: k <= (fib n.+3) by rewrite fibSS /k leq_add2l fib_monotone. rewrite {1} card_min_repE (big_cat_nat _ _ _ kl1 kl2) /=; congr addn. rewrite /k {1} fibSS !(addnC _ (fib n)) big_nat_shift card_min_repE. apply:big_nat_cond_eq => i eq1. move/andP:(eq1) => [ha]; rewrite fibSS => hb. have ww:(fib n + i - fib n.+2) = (i - fib n.+1). by rewrite -{1} (subnKC ha) addnA (addnC (fib _)) - fibSS addKn. have eq2: fib n.+2 <= fib n + i < fib n.+3. rewrite !fibSS addnC leq_add2l -addnA ltn_add2l ha /=. by apply: (leq_trans hb); rewrite leq_add2l fib_monotone. rewrite - (prednK np) in eq1. by rewrite (Zeck_S eq1) (prednK np) (Zeck_S eq2) ww. rewrite fibSS /k big_nat_shift card_min_repE. apply:big_nat_cond_eq => i /andP [ha hb]. have eq2: fib n.+2 <= fib n.+2 + i < fib n.+3. by rewrite leq_addr /= (fibSS n.+1) ltn_add2l. by rewrite (Zeck_S eq2) addKn /= eqSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)