proposition: Lemma proper_1 : forall s1, Proper (SP.Equal ==> eq) (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter s1 s2))).
proof: Proof. intros s1 x y HXY. assert (HEqI : SP.Equal (SP.inter s1 x) (SP.inter s1 y)) by (apply SPWP.inter_equal_2; assumption). apply proper_0; auto. Qed.
imports: Recdef NArith GeoCoq.Utils.sets