proposition: Lemma find_just_one_correct_aux g : size g = hw * hw -> match find_just_one g with jNone => find_all g = [::] | jOne g1 => find_all g = [:: g1] | jMore g1 g2 => [/\ g1 \in find_all g, g2 \in find_all g & g1 != g2] end.
proof: Proof. move=> Hs; rewrite /find_just_one /find_all. case: gen_init_state (gen_init_state_correct Hs) => // s1 Hs1. apply: find_just_one_aux_correct. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)