fact: Definition oextract (T : Type) (o : option T) : o -> T := if o is Some t return o -> T then fun=> t else False_rect T \o notF.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)