proposition: Lemma Zeckp_prop2 n : n = Zeckp n + Zeck_valpp (Zeck n).
proof: Proof. by rewrite - {1} (Zeck_zeck_val n) /Zeckp Zeck_valppE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)