proposition: Lemma grestrict_get_default g p q : pos2n q <= pos2n p -> get p (grestrict q g) = out.
proof: Proof. move=> qLp; rewrite /get /grestrict. case: leqP => [gLq|qLg]. by rewrite nth_default // (leq_trans gLq). by rewrite nth_cat size_take qLg ltnNge qLp /= nth_nseq if_same. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)