proposition: Lemma enum1 x : enum (pred1 x) = [:: x].
proof: Proof. rewrite [enum _](all_pred1P x _ _); first by rewrite size_filter enumP. by apply/allP=> y; rewrite mem_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)