proposition: Lemma grestrict_get g p q : pos2n p < pos2n q -> get p (grestrict q g) = get p g.
proof: Proof. move=> pLq; rewrite /get /grestrict. case: leqP => // qLg. by rewrite nth_cat size_take qLg pLq nth_take. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)