proposition: Lemma update_get p v g : size g = hw * hw -> valid_pos p -> get p (update p v g) = v.
proof: Proof. move=> Hs Hp; have := valid_pos2n Hp Hs. rewrite /update /get substE => pLs. by rewrite pLs nth_cat size_take pLs ltnn subnn. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)