proposition: Lemma Zeck_prop1 n: n != 0 -> exists a l, [/\ sorted llen (a::l), Zeck n = rev (a::l) & n = Zeck_val (a::l) ].
proof: Proof. move:(Zeck_ggen n)(Zeck_zeck_val n); case: n => // n. rewrite Zeck_S' - (revK (_ :: _)) /= rev_sorted split_rev. set u := last _ _; set v := behead _ => ra rb _. by exists u, v; split => //; rewrite - rb Zeckv_rev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)