fact: Definition refine g1 g2 := [&& size g1 == hw * hw, size g2 == hw * hw & [forall n : 'I_(hw * hw), let p := n2pos n in (get p g1 \in sref) ==> (get p g1 == get p g2)]].
imports: mathcomp(all_ssreflect) mathcomp(zify)