proposition: Lemma reduced_cons zx s : reduced (zx :: s) = [&& zx.1 != 0, zx.2 \notin predom s & reduced s].
proof: Proof. by rewrite /reduced /= andbACA [RHS]andbCA [RHS]andbA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)