proposition: Lemma max_rep_prop1 (l: seq nat): sorted gtn l -> { l' | [/\ spec_sorted l', Zeck_val l = Zeck_val l' & size l <= size l' ?= iff (spec_sorted l)] }.
proof: Proof. move => h. suff: {s: seq nat | [/\ spec_sorted s, Zeck_val l = Zeck_val s, size l <= size s ?= iff (spec_sorted l) & head 0 s <= head 0 l] }. move => [s [pa pb pc _ ]]; by exists s. elim: l h; first by move => _; exists [::]. move => a l Hrec /= h; move: (Hrec (path_sorted h)). move => [s [ha hb hc hd]]. case sa: (spec_sorted (a :: l)). by exists (a::l); split => //; apply /leqifP. case lz: (l== nil). rewrite (eqP lz) Zeckv_cons Zeckv_nil. move: sa; rewrite addn0 {1}/spec_sorted /= !eqSS - leqn1 => /negbT. rewrite (eqP lz) - ltnNge => /subnK; rewrite subn2 addn2 /= =>av. set u := ((a.-2)./2). have ww: ((a.-2 == u.*2.+1) || (a.-2 == u.*2)). by rewrite -(odd_double_half a.-2) /u;case: (odd _); rewrite eqxx // orbT. case av2: (a.-2 == u.*2.+1). + rewrite - av (eqP av2) - doubleS. move: (max_rep_fib4 u.+1); set s1 := rev _; move=> /andP [he hf]. have hg: 1 <= size s1 ?= iff false by apply /leqifP; rewrite /s1 size_rev. have hi: head 0 s1 <= (u.+1).*2.+1. rewrite /s1 /= head_rev /= last_map; case u => // v. rewrite last_iota add2n //. by rewrite - (eqP hf); exists s1. + move: ww; rewrite av2 /= => /eqP ww. rewrite - av ww - doubleS. move: (max_rep_fib3 u.+1); set s1 := rev _; move=> /andP [he hf]. have hg: 1 <= size s1 ?= iff false by apply /leqifP; rewrite /s1 size_rev. have hi: head 0 s1 <= (u.+1).*2. rewrite /s1 /= head_rev /= !last_map; case u => // v. by rewrite last_iota add1n ltn_double. by rewrite - (eqP hf); exists s1. set b := head 0 l. set c := head 0 s. have pa: l = b:: behead l by move: lz; rewrite /b; case l. have pb: s = c:: behead s by move:hc => []; rewrite pa /c; case s. rewrite -/c -/b in hd. have lba: b < a by move: h; rewrite pa /= => /andP []. case wa: (gespec a c). have ra: spec_sorted (a :: s). by move:ha wa; rewrite pb /spec_sorted /= ; move => /andP[ -> ->] ->. have rb: ((a == b.+1) || (a == b.+2)). rewrite (eqn_leq _ b.+1) (eqn_leq _ b.+2) lba. by case/orP: wa => /eqP ->; rewrite! ltnS hd //= andbT (ltnNge c) orNb. exists(a:: s); rewrite !Zeckv_cons hb /= leqnn; split => //. move: hc; move: sa; rewrite /spec_sorted pa /= rb /= => ->. by move /leqifP => H; apply/leqifP; rewrite ltnS. have lac: c.+2 < a. move: (leq_ltn_trans hd lba); rewrite leq_eqVlt; case /orP. by rewrite eq_sym => h1; move: wa; rewrite /= h1. rewrite leq_eqVlt; case /orP => //. by rewrite eq_sym => h1; move: wa; rewrite /= h1 orbT. set n := (a -c.+1)./2; set k := a - n.*2. have [kp1 /eqP kp2]: ((k == c.+1) ||(k == c.+2)) /\ (k + n.*2 == a). move: (subnK lac); set v := a -c.+3; rewrite - {1} add2n addnA addn2 => v1. rewrite /k /n -v1 addnK -{1 3 5 8} (odd_double_half v.+2). case: (odd _); first by rewrite add1n addSnnS addKn addnC !eqxx orbT. by rewrite addKn addnC !eqxx. case: (posnP n) => np. move:kp1 lac; rewrite /k np subn0; case ww: (a==c.+2). by rewrite (eqP ww) ltnn. by rewrite orbF => /eqP -> /ltnW; rewrite ltnn. move: (fib_partial_sum' k n) => []; cbv zeta; set l1 := _ :: _. rewrite addSn addSn kp2 Zeckv_cons => <- => he. exists (rev l1 ++ s). split => //. + move: he ha; rewrite /l1; set l2 := mkseq _ _; move: (split_rev k l2) => eq1. rewrite /spec_sorted {1 2} eq1 /= cat_path => -> /=. rewrite last_cat rev_cons last_rcons pb /= => /andP[-> ->]. set x := last _ _. have: x = last k (rev (k :: l2)) by rewrite eq1 /x rev_cons. by rewrite rev_cons last_rcons ! andbT => ->. + by rewrite hb /Zeck_val big_cat sum_rev. + apply /leqifP; rewrite size_cat size_rev /l1/size_cat /= size_mkseq. by rewrite -(prednK np) addSn addSn ltnS ltnS (leq_trans hc) // leq_addl. + rewrite /l1 /= rev_cons cat_rcons -(prednK np)- (revK (k::s)) - rev_cat. rewrite head_rev last_cat last_mkseq add0n - kp2 -{2} (prednK np) doubleS. by rewrite addnS addnS addSn ltnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)