fact: Definition pick_varieties (ss : SS.t) (st : STt) : (option (SS.elt * SS.elt)) := match (exists_witness (fun s => match (pick_varieties_aux s (SS.remove s ss) st) with | None => false | _ => true end) ss) with | None => None | Some s1 => pick_varieties_aux s1 (SS.remove s1 ss) st end.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets