proposition: Lemma ZeckM_fibm2 n: ZeckM (fib (n.+3)).-2 = rev (iota 0 n).
proof: Proof. apply:ZeckM_prop3; apply/andP; split. rewrite spec_sorted_rev; case: n => // n /=; rewrite andbT. by elim:n (0) => // k H n /=; rewrite H eqxx. rewrite /Zeck_val - fib_sum !big_ord_recl /=. elim:n => [|n Hr];first by rewrite big_nil big_ord0. by rewrite big_ord_recr - (eqP Hr) iota_Sr rev_rcons big_cons addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)