proposition: Lemma enum_ordSr : enum 'I_n = rcons (map (widen_ord (leqnSn _)) (enum 'I_n')) ord_max.
proof: Proof. apply: (inj_map val_inj); rewrite val_enum_ord. rewrite -[in iota _ _]addn1 iotaD/= cats1 map_rcons; congr (rcons _ _). by rewrite -map_comp/= (@eq_map _ _ _ val) ?val_enum_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)