proposition: Lemma card_min_repn1 n: card_min_rep n 1 = (2 <=n).
proof: Proof. case: n=> [|[|n]]; rewrite ? card_min_rep0m ?card_min_rep1m //=. rewrite card_min_repE big_ltn_cond ?fib_smonotone_bis // Zeck_fib /=. rewrite big_hasC => //; apply /hasPn => i. rewrite mem_index_iota=> /andP[ha hb]; move:(Zeck_zeck_val i). case:(Zeck i) => // a [|b l //]; rewrite Zeckv_cons Zeckv_nil addn0 => h. move:hb; rewrite - h => /fib_monotone_bis; rewrite ltnS => /fib_monotone. by rewrite h leqNgt ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)