proposition: Lemma Zeck_valp_aux l: sorted gtn l -> exists (l': seq nat), [/\ sorted ggen l', odd_last l = odd_last l', Zeck_val l = Zeck_val l', Zeck_valp l = Zeck_valp l' & size l' <= size l ?= iff (sorted ggen l)].
proof: Proof. have Hb a s: Zeck_valp (a::s) = fib (a.+1) + Zeck_valp s. by rewrite /Zeck_valp big_cons. pose z l := (Zeck_val l, Zeck_valp l, odd_last l). have He a l1 : z [:: a.+1, a & l1] = z (a.+2 :: l1). have od: odd (last a.+2 l1)= odd (last a l1) by case: l1 => //=;case: odd. by rewrite /z !Zeckv_cons !Hb addnA addnA - !fibSS /= od. have Hf a l1 l2: z l1 = z l2 -> z (a :: l1) = z (a::l2). rewrite /z !Zeckv_cons !Hb; case => eq1 eq2 eq3; rewrite eq1 eq2 /=. suff: odd (last a l1) = odd (last a l2) by move => ->. move: eq1 eq3; clear; case: l1; case: l2 => //. + by move => u v h;move:(Zeckv_pos u v); rewrite -h Zeckv_nil. + by move => u v h;move:(Zeckv_pos u v); rewrite h Zeckv_nil. + by move => u la v lb //= _; case:odd; case:odd. suff H: forall (a:nat) l, sorted gtn (a :: l) -> exists (b:nat) s, [/\ sorted ggen (b::s), z(a::l) = z(b::s), b <= a.+1 & size s <= size l ?= iff sorted ggen (a::l) ]. case: l => //; first by move => _; exists nil. by move => a l /H [b [s [pa [pb pc pd _] pf]]]; exists (b::s). move => {l} a l. move: {2} ((size l).+1) (ltnSn (size l))=> n; elim: n a l; first by case. move => n Hrec a [_ _ | b l ]; first by exists a, nil. rewrite /= ltnS => lt1 /andP [lt2 pa]. move: lt2; rewrite leq_eqVlt; case /orP => [/eqP <- | lt3]. move: l lt1 pa; case; first by exists (b.+2), nil; rewrite ltnn. move => c l /= pa /andP [pb pc]. move: (Hrec c l (ltn_trans (ltnSn (size l)) pa) pc). move => [u [v [/= qa qb qc qd]]]; exists (b.+2), (u::v). rewrite He (Hf b.+2 _ _ qb) /= qa ! ltnS (leq_trans qc pb) ltnn. by split => //; apply/leqifP; rewrite !ltnS /= qd. case ww: (path ggen b l). by exists a, (b::l);rewrite /= lt3 ww; split => //; apply /leqif_refl. move: (Hrec b l lt1 pa) => [c [l' [r1 /(Hf a _ _ ) -> r4]] sc]. move:(leq_ltn_trans r4 lt3); rewrite leq_eqVlt; case /orP => lt4; last first. by exists a, (c:: l'); rewrite /= lt4 lt3 /= -ww mono_leqif. exists (a.+1), l'; rewrite - (eqP lt4) He andbF. move: sc; rewrite /sorted ww => /leqifP => /ltnW ss. have K:size l' <= (size l).+1 ?= iff false by apply /leqifP; rewrite ltnS. split => //; move: r1; case l' => // d l'' /= /andP[ w ->]. by rewrite (ltn_trans w (ltn_trans (ltnSn c) (ltnSn c.+1))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)