fact: Fixpoint find_one_aux (n : state) (g : seq nat) (st : state) {struct n} : option (seq nat) := if st is (_, p, vs) :: st1 then if n is _ :: n1 then try_one (behead vs) p 1 g st1 (find_one_aux n1) else None else some g.
imports: mathcomp(all_ssreflect) mathcomp(zify)