proposition: Lemma refineP g1 g2 : reflect [/\ size g1 = hw * hw, size g2 = hw * hw & forall p, valid_pos p -> get p g1 \in sref -> get p g1 = get p g2] (refine g1 g2).
proof: Proof. apply: (iffP and3P) => [[/eqP Heq1 /eqP Heq2 /forallP /= Hf]| [Heq1 Heq2 Hf]]; split => //; try by apply/eqP. move=> [x y] Hp. have /implyP := Hf (Ordinal (valid_pos_pos2n_lt Hp)). rewrite /get pos2nK /= //. by move=> Hk Hg; have /eqP := (Hk Hg). by apply: valid_pos_pos2n_lt. apply/forallP=> /= n; rewrite /get pos2nK //. have hw_pos : 0 < hw. suff : 0 < hw * hw by case: hw. by apply: leq_ltn_trans (ltn_ord n). apply/implyP => Hg; apply/eqP. have := Hf (n2pos n). rewrite /get pos2nK //; apply => //. rewrite /valid_pos /= ltn_mod. by rewrite ltn_divLR ?ltn_ord /=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)