proposition: Lemma in_state_init n p bs : (n, p, bs) \in init_state = [&& n == hw, valid_pos p & bs == false :: nseq hw true].
proof: Proof. have rE : rank_val (false :: nseq hw true) = hw. by rewrite /rank_val /= count_nseq mul1n. apply/mapP/idP => /= [[[x y]] /= Hc [-> -> ->] | /and3P[/eqP-> Hc /eqP->]]. by rewrite rE -mem_cross2 Hc !eqxx. by exists p; rewrite ?rE ?mem_cross2. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)