proposition: Lemma FR_prop4 m: llen 1 (Zeck_li m) ->FR (Zeckp m).+1 = FR (Zeckp (Zeckp m)).
proof: Proof. move => Hm;move: (Hm); rewrite /llen /ggen /= => /Zeck_li_prop2 Hm1. rewrite /= FR_prop1 //; move: Hm Hm1; rewrite /Zeck_li; case: m => // m. move: (Zeck_prop1 (n:=m.+1) isT) => [a [l [pa -> ->]]]. rewrite {1} rev_cons last_rcons => sc sd. have: all (leq 1) (rev (a:: l)) by apply /allP; move => x /(allP sd)/ltnW/ltnW. move /(seq_prednK); set s' := (pred_seq (rev (a :: l))) => sv'. have sv:sorted ggen (rcons s' 0). have aa: (rev (succ_seq (rcons s' 0))) = [:: 1, a & l]. by rewrite /succ_seq map_rcons -/(succ_seq s') - sv' - rev_cons revK. by rewrite -sorted_ggen_succ - rev_sorted aa /=; apply/andP. have eq: (Zeck_valp (a :: l)).+1 = Zeck_val (rcons s' 0). by rewrite /Zeck_valp /Zeck_val sum_rcons - sum_rev sv' big_map. by rewrite (Zeckp_prop1 (sorted_llen_uniq pa)) eq (ZeckP sv) last_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)