proposition: Lemma inj_widen_ord n m (h : n <= m) : injective (widen_ord h).
proof: Proof. move => x y hxy. have /= {}hxy : widen_ord h x = widen_ord h y :> nat by rewrite hxy. by apply/ord_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)