proposition: Lemma invariant_init : invariant init_state ginit.
proof: Proof. split. - by rewrite size_ginit. - split; first by rewrite spos_init_state cross2_uniq. by move=> p; rewrite spos_init_state mem_cross2. move=> p z. rewrite /init_state. elim: cross2 => //= p1 cross2 IH . case/orP => [/andP[_]|]; last first. by apply: IH => // p2 Hp2; apply: Hc; rewrite in_cons Hp2 orbT. case: (z) => [|z1]; rewrite /in_val //= nth_nseq mem_iota add1n !ltnS /=. by case: leqP. - by move=> p Hp; rewrite (negPf (get_init _)) spos_init_state mem_cross2 Hp. - by move=> p1 p2; rewrite (negPf (get_init _)). split. by move=> p1 p2; rewrite (negPf (get_init _)). by move=> p1 z1 Hp1 Hz1; rewrite in_state_init_state. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)