proposition: Lemma Zeck2_unique (s s': seq nat) : sorted ggen s -> sorted ggen 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. elim: s' s; first by case => // a l _ _; move/ esym /A. move => a l Hrec; case; first by move => _ _ /A. move => a' l'; rewrite !Zeckv_cons => pa pb ec. suff aux:(a' == a). move /eqP: ec; rewrite (eqP aux) eqn_add2l => /eqP h. by rewrite (Hrec l' (path_sorted pa) (path_sorted pb) h). move:(Zeckv_bound2 pa); rewrite Zeckv_cons ec. move/ (leq_ltn_trans (leq_addr (Zeck_val l) (fib a.+2))) => /fib_monotone_bis. move:(Zeckv_bound2 pb); rewrite Zeckv_cons -ec. move/ (leq_ltn_trans (leq_addr (Zeck_val l') (fib a'.+2))) => /fib_monotone_bis. by rewrite !ltnS eqn_leq => -> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)