proposition: Lemma max_rep_unique (s s': seq nat) : spec_sorted s -> spec_sorted s' -> Zeck_val s = Zeck_val s' -> s = s'.
proof: Proof. have A a l: Zeck_val [::] = Zeck_val (a :: l) -> False. by rewrite Zeckv_nil => h; move: (Zeckv_pos a l); rewrite - h. have B a l: spec_sorted (a::l) -> (fib a.+3) <= (Zeck_val (a::l)).+1 < (fib a.+4). by rewrite fib_pos(fib_pos a.+3) !ltnS => /max_rep_bound. elim: s' s; first by case => // a l _ _; move/ esym /A. move => a l Hrec [_ _ /A //| a' l' sa sb sc]. move: (B _ _ sa); rewrite sc => sa'. move /eqP: (fib_partition sa' (B _ _ sb)); rewrite !eqSS => /eqP aux. move: sa sb sc; rewrite aux ! spec_sorted_rec => /andP[ _ hc] /andP[ _ hd]. by move /eqP; rewrite !Zeckv_cons eqn_add2l => /eqP h; rewrite (Hrec l'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)