fact: Definition eqopp (p1 p2 : option (SS.elt * SS.elt)) := match p1,p2 with | None, None => True | Some s1, Some s2 => True | _, _ => False end.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets