fact: Fixpoint preim_seq s := if s is y :: s' then (if pick (preim f (pred1 y)) is Some x then cons x else id) (preim_seq s') else [::].
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)