proposition: Lemma lift_pred_widen_ord m n (h : n <= m) : lift_pred (widen_ord h) =1 widen_ord (size_tool h).
proof: Proof. rewrite /lift_pred => x; have [y hx|y hx] := splitP; apply/ord_inj => //=. by rewrite hx [y]ord1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)