proposition: Lemma enum_ordSl : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n').
proof: Proof. apply: (inj_map val_inj); rewrite val_enum_ord /= -map_comp. by rewrite (map_comp (addn 1)) val_enum_ord -iotaDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)