proposition: Lemma grestrict_size p g : size (grestrict p g) = (size g).
proof: Proof. rewrite /grestrict; case: leqP => // pLg. by rewrite size_cat size_take pLg size_nseq addnC subnK // ltnW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)