proposition: Lemma Zeckp_prop6 n m q (s := pred_seq (Zeck m)): n = m + fib q.+3 -> (m = 0 \/ llen q.+1 (Zeck_li m)) -> [/\ Zeck (Zeckp n) = rcons (Zeck (Zeckp m)) q, (q >0 -> Zeck (Zeckp (Zeckp n)) = rcons (Zeck (Zeckp (Zeckp m))) q.-1), sorted llen (q :: rev s), Zeckp m = Zeck_val (rev s) & Zeckp n = fib q.+2 + Zeckp m].
proof: Proof. move => sa sb; rewrite /s. move:(Zeck_zeck_val m) (Zeck_ggen m) sb; rewrite /Zeck_li. set l := (Zeck m) => qa qb; case => qc. rewrite /l sa qc /= !Zeckp_0 Zeck_0 !Zeckp_fib !Zeck_fib Zeckv_nil addn0. by split => // /prednK {1} <-; rewrite Zeck_fib. have lp0: 1 < last m l by apply: (leq_trans _ qc); rewrite !ltnS leq0n. move:(Zeck_li_prop2 (ltnW lp0)) => lp1. have qd: sorted llen (q.+1 :: rev l). move: qb qc; rewrite - rev_sorted -/llen - qa - {2 3} (revK l). by case: (rev l) => // u v; rewrite rev_cons last_rcons /= => -> ->. move: (seq_prednK lp1); rewrite -/s => eq1. have qg: sorted llen (q :: rev s). by move:qd; rewrite /l eq1 -map_rev -map_cons -/(succ_seq _) sorted_llen_succ. have qg':sorted ggen s by rewrite - rev_sorted; apply: (path_sorted qg). have qe: m = Zeck_val (rev l) by rewrite - qa /Zeck_val sum_rev. have qe': Zeck_valp s = Zeck_valp (rev s) by rewrite /Zeck_valp sum_rev. have eq2: Zeckp m = Zeck_val (rev s). rewrite qe /Zeck_val !sum_rev (Zeckp_prop0 (sorted_ggenW qb)) /l eq1. by rewrite /Zeck_valp big_map. move: (Zeck_split qd (leqnn (fib q.+3))). rewrite - qe addnC - sa Zeckp_fib => eq3. rewrite - eq3 - eq2 qg. have sv: Zeck (Zeckp m) = s by rewrite eq2 /Zeck_val -sum_rev ZeckP revK. have eq4: Zeck (Zeckp n) = rcons s q. move: qg; rewrite - rev_sorted rev_cons revK => /ZeckP <- //. by rewrite eq3 /Zeck_val sum_rcons eq2 /Zeck_val sum_rev. rewrite {3 5} /Zeckp sv eq4 qe'; split => //. have lp2: all [pred z | 0 < z] s. apply /allP => [z /mapP [x /(allP (Zeck_li_prop2 lp0)) /=]]. by case x => // m';rewrite ltnS succnK => h ->. move: (seq_prednK lp2); set s' := [seq i.-1 | i <- s] => sv' qp. move: qg ; rewrite - {1 2} (prednK qp) => qg. have qg'': sorted llen (q.-1 :: rev s'). move: qg; rewrite sv' - map_rev /llen /=. by elim: (rev s') (q.-1) => // u v H b /= /andP[h /H ->];rewrite -ltnS h. have qg''':sorted ggen s' by rewrite - rev_sorted; apply: (path_sorted qg''). rewrite/Zeck_valp sv' - map_rev big_map sum_rev (ZeckP qg''') sum_rcons. by rewrite big_map - (sum_rcons q.-1) ZeckP // - rev_sorted rev_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)