proposition: Lemma DUR_fib i : v i = fib i.+2.
proof: Proof. move:i. have Ha l i a: i \in a :: l -> path gtn a l -> i <= a. rewrite inE; case/orP; first by move /eqP => ->. elim:l i a => // a l H i b /= h /andP [ha hb]; move:h; rewrite inE. case/orP; [ by move/eqP ->; apply: ltnW |move => il;apply:H => //]. move: ha hb; case l => // a' l' /= ha /andP [hb ->]. by rewrite (ltn_trans hb ha). have Hb k: (forall i, i < k.*2 -> v i = fib i.+2) -> (v k.*2.+1 < fib k.*2.+1 \/ (v k.*2 = fib k.*2.+2 /\ v k.*2.+1 < fib k.*2.+3)) -> False. move => Hrec lta;case /andP: (max_rep_fib2 k.+1). case/andP: (max_rep_fib2 k); set l' := rev _; set l := rev _. move => _ /eqP zvl' ssl /eqP zvl. have lt1:v k.*2.+1 < fib k.*2.+3. case: lta; last by case. move =>h;apply: (leq_trans h); by apply: fib_monotone;apply: ltnW => //. have lv: l = k.*2.+1 :: l'. rewrite /l /l' /mkseq iota_Sr /succ_seq - !map_comp /comp - !map_rev. by rewrite rev_rcons. set s := \sum_(i <- l) v i; set s' := Zeck_val l. have eqr: \sum_(i <- l') v i = Zeck_val l'. rewrite /Zeck_val /l' ! sum_rev /mkseq /succ_seq !big_map. apply: eq_big_seq => i; rewrite mem_iota /= add0n => ik. by apply: Hrec; rewrite ltn_Sdouble. move: (ZeckM_prop2 s); set z := ZeckM s; move /andP => [ssz /eqP]. move: ssz; case:z. rewrite Zeckv_nil /s lv big_cons => _ /eqP; rewrite eq_sym addn_eq0. by move/andP => [/eqP h _]; move:(DUR_positive k.*2.+1); rewrite h. move => hz tz ssz zv. move:(max_rep_bound ssz); rewrite zv; move => /andP [le2 _ ]. have: s < s' by rewrite /s/s' lv Zeckv_cons big_cons eqr ltn_add2r. move/(leq_ltn_trans le2); rewrite /s' zvl - ltnS - fib_pos // - fib_pos //. move/fib_monotone_bis; rewrite doubleS !ltnS => hm. suff Hz: forall i, i <= hz -> v i = fib i.+2. have eq2: Zval_v (hz :: tz) = Zval_v l. rewrite -[RHS] zv /Zeck_val /Zval_v;apply: eq_big_seq => i il. exact (Hz _ (Ha _ _ _ il (spec_sorted_sorted ssz))). move:(v_unique ssz ssl eq2);rewrite lv; case => eq3. by move: hm; rewrite eq3 ltnn. case: lta; last first. move => [pa pb] i li; move: (leq_trans li hm); rewrite leq_eqVlt. by case/orP; [ move/eqP => -> // | apply/ Hrec ]. move => la. have: s < (fib k.*2.+3).-1. rewrite /s lv big_cons eqr zvl' (fibSS k.*2.+1) {2} (fib_pos k.*2.+1). by rewrite addSn addnC ltn_add2l. move/(leq_ltn_trans le2); rewrite - ltnS - fib_pos //- fib_pos //. move/fib_monotone_bis;rewrite !ltnS => hm1 i ih; apply: Hrec. apply: (leq_ltn_trans ih hm1). have Hc k: (forall i, i < k.*2.+1 -> v i = fib i.+2) -> (v k.*2.+2 < fib k.*2.+2 \/ (v k.*2.+1 = fib k.*2.+3 /\ v k.*2.+2 < fib k.*2.+4)) -> False. move => Hrec lta; case /andP: (max_rep_fib1 k.+2). case /andP: (max_rep_fib1 k.+1); set l' := rev _; set l := rev _. move => _ /eqP zl' ssl /eqP zvl. have lv: l = k.+1.*2 :: l' by rewrite /l/l'/mkseq iota_Sr -!map_rev rev_rcons. set s := \sum_(i <- l) v i; set s' := Zeck_val l. have lt1:v k.*2.+2 < fib k.*2.+4. case: lta; last by case. move =>h;apply: (leq_trans h); by apply: fib_monotone;apply: ltnW => //. have eqr: \sum_(i <- l') v i = Zeck_val l'. rewrite /Zeck_val /l' ! sum_rev /mkseq /succ_seq !big_map. apply: eq_big_seq => i; rewrite mem_iota /= add0n => ik. by apply: Hrec; rewrite ltnS leq_double - ltnS. move: (ZeckM_prop2 s); set z := ZeckM s; move /andP => [ssz /eqP]. move: ssz; case:z. rewrite Zeckv_nil /s lv big_cons => _ /eqP; rewrite eq_sym addn_eq0. by move/andP => [/eqP h _]; move:(DUR_positive (k.+1).*2); rewrite h. move => hz tz ssz zv. move:(max_rep_bound ssz); rewrite zv; move => /andP [le2 _ ]. have: s < s' by rewrite /s/s' lv Zeckv_cons big_cons eqr ltn_add2r. move/(leq_ltn_trans le2); rewrite /s' zvl - ltnS - fib_pos // - fib_pos //. move/fib_monotone_bis; rewrite doubleS 3!ltnS => hm. suff Hz: forall i, i <= hz -> v i = fib i.+2. have eq2: Zval_v (hz :: tz) = Zval_v l. rewrite -[RHS] zv /Zeck_val /Zval_v;apply: eq_big_seq => i il. exact (Hz _ (Ha _ _ _ il (spec_sorted_sorted ssz))). move:(v_unique ssz ssl eq2);rewrite lv; case => eq3. by move: hm; rewrite eq3 ltnn. case: lta; last first. move => [pa pb] i li; move: (leq_trans li hm); rewrite leq_eqVlt. by case/orP; [ move/eqP => -> // | apply/ Hrec ]. move => la. have: s < (fib k.*2.+4).-1. rewrite /s lv big_cons eqr zl' (fibSS k.*2.+2) {2} (fib_pos k.*2.+2). by rewrite addSn addnC ltn_add2l. move/(leq_ltn_trans le2); rewrite - ltnS - fib_pos //- fib_pos //. move/fib_monotone_bis;rewrite !ltnS => hm1 i ih; apply: Hrec. by rewrite ltnS (leq_trans ih hm1). have Hj a l: spec_sorted l -> a \in l -> exists w L, spec_sorted (a :: L) /\ l = w ++ (a :: L). elim: l a => [ a // | b l H a ha]. rewrite inE; case/orP; first by by move => /eqP ->; exists nil, l. move: ha; rewrite spec_sorted_rec => /andP[_] ha hb; move:(H _ ha hb). by move => [w [L [hc ->]]]; exists (b::w), L. move => i. move:DUR_01 =>[v0 v1]. elim: i {-2} i (leqnn i); first by move => i; rewrite leqn0 => /eqP -> //. move => n Hrec n1; rewrite leq_eqVlt; case/orP=> [|Hn]; last first. by apply: Hrec; rewrite -ltnS. move/eqP ->; clear n1. case: (ltngtP (v n.+1)(fib n.+3)) => // lt1. case: (odd_dichot n.+1); set k := (n.+1)./2 => nv. move: nv => /eqP;rewrite eqSS => /eqP nv; case: (Hb k). by rewrite - nv; move => i /ltnW /Hrec. by right; rewrite - nv; split => //; apply: Hrec. have nv2: n = (k.-1).*2.+1. by move: nv; case:k => // k /= /eqP; rewrite doubleS eqSS => /eqP. case: (Hc k.-1). by move => i; rewrite -nv2 => /ltnW/Hrec. by right; rewrite - nv2; split => //; apply: Hrec. move: lt1;case: (ltngtP (fib n.+3) (v n.+1)) => // lt2 _. move:(fib_sum_alt n.+1); rewrite - Zeckv_rev; set l := rev (iota 0 n.+1) => xm1. have eq2: Zval_v l = Zeck_val l. rewrite /Zeck_val /Zval_v; apply: eq_big_seq => i il; apply/ Hrec. by move: il; rewrite /l mem_rev mem_iota /= ltnS. set x := (Zval_v l).+1; move: (v_exists x) => [L]. case:L =>[ |a L ss sv]; first by rewrite/Zval_v big_nil /x. have Hi k: (fib k.+4).-2.+2 = fib k.+4. have: fib 3 < fib k.+4 by apply:fib_smonotone_bis. by move/ltnW /subnK; rewrite subn2 addn2. case: (leqP a n) => can. have eq1: Zval_v (a :: L) = Zeck_val (a :: L). rewrite /Zeck_val /Zval_v; apply: eq_big_seq => i il. move:(leq_trans (Ha _ _ _ il (spec_sorted_sorted ss)) can); apply: Hrec. move: (max_rep_bound ss); rewrite - eq1 sv /x eq2 xm1. move /andP => [_]. rewrite - ltnS Hi - fib_pos => /fib_monotone_bis. by rewrite !ltnS ltnNge can. case nl: (n.+1 \in (a::L)). move:(Hj _ _ ss nl) => [w [l1 [sl1 l1v]]]. have eq3: \sum_(j <- l1) v j = Zeck_val l1. rewrite /Zeck_val; apply: eq_big_seq => i. move: sl1; rewrite spec_sorted_rec; case/andP =>[]. case l1 => // b l2 /= pa pb pc; apply: Hrec. apply: (leq_trans (Ha _ _ _ pc (spec_sorted_sorted pb))). by move:pa; rewrite !eqSS; case/orP => /eqP ->. have lta: Zeck_val (n.+1::l1) <= (fib n.+4).-2. move: lt2; rewrite -(ltn_add2r ( Zeck_val l1));rewrite Zeckv_cons => h. rewrite - ltnS;apply: (leq_trans h); rewrite -xm1 - eq2 -eq3 -/x -sv. by rewrite /Zval_v l1v big_cat big_cons/=; apply: leq_addl. move: (max_rep_bound sl1) => /andP [hh _]. by move: (leq_trans hh lta);rewrite - {1} Hi /= ltnn. case nl2: (n.+2 \in (a::L)); last first. move:(negbT nl2); move/negP; case; move: ss can nl; clear. elim: L a n. move => a n;rewrite spec_sorted_rec /= => /andP[la1 _] na. move:(leq_trans na la1); rewrite ltnS leqn0 => nz. by move: la1 na; rewrite (eqP nz) inE; case a => //; case. move => a l Hrec b n; rewrite spec_sorted_rec /= => /andP[ha hb]. rewrite inE leq_eqVlt; case: (n.+1 == b) => //=;rewrite leq_eqVlt !inE. case: (n.+2 == b) => //=; move => nb; apply: Hrec => //. by move: nb; case /orP: ha => /eqP -> // h; apply: ltnW. move: (Hj _ _ ss nl2) => [w [l2 [sa sb]]]. move: nl; rewrite sb; rewrite mem_cat => /norP [_] nl. move: sa sb nl; rewrite spec_sorted_rec; case: l2 => // b l2 /=. rewrite !inE !eqSS => /andP []; case/orP; first by move => -> //=;rewrite orbT. move => /eqP <- => pa pb _. move: (max_rep_bound pa) => /andP [lt1 _]. have pc: \sum_(j <- (n :: l2)) v j = Zeck_val (n :: l2). rewrite /Zeck_val; apply: eq_big_seq => i il; apply: Hrec. exact: (Ha _ _ _ il (spec_sorted_sorted pa)). move: sv; rewrite pb /Zval_v big_cat /= big_cons pc /x eq2 xm1 => sa. move:(leq_addl (\sum_(i <- w) v i) (v n.+2 + Zeck_val (n :: l2))). rewrite sa fibSS fib_pos addSn (fib_pos n.+1) addnS /= -addnS - fib_pos => lt3. move: lt1; rewrite - (leq_add2r (fib n.+2)) => lt4. move:(leq_trans lt3 lt4); rewrite addnC leq_add2l leq_eqVlt. have W: forall k, k.+2 = k -> False by elim => // k H; case. case: eqP; first by rewrite -(Hrec n (leqnn n)) => /DUR_injv // /W. move => _ /= Hx. case: (odd_dichot n.+2); set k := (n.+2)./2 => nv. move: nv => /eqP;rewrite eqSS => /eqP nv; case: (Hb k); rewrite - nv //. by left. move: (Hc k.-1). have <-: n = (k.-1).*2. by move: nv; case:k => // k /= /eqP; rewrite doubleS !eqSS => /eqP. by case => //; left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)