fact: Definition pick_lengths (ss : SSP.t) : (option (SSP.elt * SSP.elt)) := match (exists_witness (fun s => match (pick_lengths_aux s (SSP.remove s ss)) with | None => false | _ => true end) ss) with | None => None | Some s1 => pick_lengths_aux s1 (SSP.remove s1 ss) end.
imports: Recdef NArith GeoCoq.Utils.sets