fact: Definition pick_lines_aux (s1 : SS.elt) (ss : SS.t) (sp : SP.t) : (option (SS.elt * SS.elt)) := match ((exists_witness (fun s2 => let i := S.inter s1 s2 in pick_line i sp)) ss) with | None => None | Some s2 => Some(s1,s2) end.
imports: Recdef NArith GeoCoq.Utils.sets