proposition: Lemma refine_init g : size g = hw * hw -> refine ginit g.
proof: Proof. move=> Hs; apply/refineP; split => //; first by apply size_ginit. move=> p _; rewrite /ginit /get !nth_nseq if_same => H. by case/negP: out_not_in_refl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)