proposition: Lemma grestrict_update p g : pos2n (next p) <= size g -> grestrict (next p) g = update p (get p g) (grestrict p g).
proof: Proof. rewrite /grestrict /get /update substE next_pos. rewrite leq_eqVlt => /orP[/eqP He|pLg]. have pLg : pos2n p < size g by rewrite He. rewrite He ltnn eqxx /= size_cat size_take. rewrite size_nseq pLg addnC subnK; last by rewrite ltnW. rewrite leqnn take_cat size_take pLg ltnn subnn take0 cats0. rewrite drop_cat size_take pLg ltnNge (ltnW pLg) /= drop_nseq subnn //=. rewrite -[LHS](cat_take_drop (pos2n p)) //. by rewrite (drop_nth out) // drop_oversize // He. have pLg1 : pos2n p < size g by rewrite ltnW. rewrite pLg orbT size_cat size_nseq size_take pLg1 ifT; last first. by rewrite addnC subnK // ltnW. rewrite take_cat drop_cat !size_take !pLg1 ltnn ifN -?leqNgt ?leqnS //. rewrite subSn // subnn take0 cats0 drop_nseq subn1 subnS. by rewrite -cat_rcons (take_nth out). Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)