proposition: Lemma val_ord_enum : map val ord_enum = iota 0 n.
proof: Proof. rewrite pmap_filter; last exact: insubK. by apply/all_filterP; apply/allP=> i; rewrite mem_iota isSome_insub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)