proposition: Lemma Zeck_is_minimal l n (L := Zeck n): sorted gtn l -> Zeck_val l = n -> size L <= size l ?= iff (l == L).
proof: Proof. move => ha hb; apply /leqifP. move: (Zeck_valp_aux ha) => [ s [ /ZeckP pa _ pc _]]. rewrite -pa - pc hb -/L; move /leqifP. case wx: (sorted ggen l); first by rewrite - (ZeckP wx) hb !eqxx. by case wy: (l == L) => //; rewrite (eqP wy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)