proposition: Lemma widen_ord_eq (m n : nat) (h h' : n <= m) : widen_ord h =1 widen_ord h'.
proof: Proof. by move=> x; 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)