proposition: Lemma size_tool n k : k <= n -> k < n.+1.
proof: Proof. by rewrite ltnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)