proposition: Lemma ord_enum_eqE p : ord_enum_eq p = enum 'I_p.
proof: Proof. by rewrite enumT unlock; apply:eq_pmap ; exact:insub_eqE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly matrix mxpoly) CoqEAL(hrel param refinements trivial_seq)