proposition: Lemma unique_representation n: (exists k, n = (fib k.+2).-1) <-> (forall l l', sorted gtn l -> Zeck_val l = n -> sorted gtn l' -> Zeck_val l' = n -> l = l').
proof: Proof. split. move => [k nv]. have pa: Zeck n = ZeckM n. case: (odd_dichot k) => kv. have ->: n = (fib((k./2.+1).*2.+1)).-1 by rewrite nv {1} kv /= doubleS. by rewrite (ZeckM_prop3 (max_rep_fib1 (k./2.+1))) -(Zeck_fib1 (k./2.+1)). by rewrite nv kv (ZeckM_prop3 (max_rep_fib2 k./2)) (Zeck_fib2 k./2). have pb: (size (Zeck n) = size (ZeckM n)) by rewrite pa. move => l l' la ea lb eb. by rewrite (proj2 (ZeckM_prop4 la ea) pb) (proj2 (ZeckM_prop4 lb eb) pb). move => H. move: (ZeckM_prop2 n) => /andP [/spec_sorted_sorted ha /eqP hb]. move: (sorted_ggenW (Zeck_ggen n)) => hc. move: (Zeck_zeck_val n) => hd; rewrite - hd. move: (ZeckM_prop1 n)=> []; rewrite (H _ _ ha hb hc hd) => [he _ _]. case: (posnP n) => np. by exists 0; rewrite np Zeckv_nil. rewrite lt0n in np;move: (Zeck_prop1 np) => [a [l [pa pb pc]]]. suff: a::l = (mkseq double (size l).+1) \/ a ::l = (succ_seq (mkseq double (size l).+1)). rewrite pb; case => ->. by exists ((size l).*2.+1); rewrite -Zeck_fib1 Zeck_zeck_val. by exists ((size l).*2.+2); rewrite -Zeck_fib2 Zeck_zeck_val. move: he pa; rewrite pb spec_sorted_rev /= !eqSS. move => /andP [pd pe] pf. suff: a :: l = [seq i+a | i<- mkseq double (size l).+1]. move => ->; rewrite /mkseq /succ_seq -!map_comp /comp. case: (orP pe) => av; rewrite (eqP av); [left | right]. by apply/eq_in_map => i _; rewrite addn0. by simpl; congr cons; apply/eq_in_map => i _; rewrite addn1. move: pd pf; clear; elim: l a => [a // | a l Hr b]. simpl => /andP[ ha hb] /andP[hc hd]. case: (orP ha) => ha'; first by move: hc; rewrite (eqP ha') ltnn. rewrite Hr //= (eqP ha') (iota_S 1) /succ_seq -! map_comp /comp /=. by congr cons; congr cons; apply/eq_in_map => i _;rewrite !addnS ! addSn //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)