proposition: Lemma Some_oextract T (x : option T) (x_ex : x) : Some (oextract x_ex) = x.
proof: Proof. by case: x x_ex. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)