proposition: Lemma proper_00 : forall s, Proper ((fun t1 t2 : SetOfPairsOfPositiveOrderedType.t => Pos.eq (fstpp t1) (fstpp t2) /\ Pos.eq (sndpp t1) (sndpp t2)) ==> eq) (fun p : SP.elt => S.mem (fstpp p) s && S.mem (sndpp p) s).
proof: Proof. intros s x y Hxy. destruct Hxy as [Hxyfst Hxysnd]. rewrite Hxyfst. rewrite Hxysnd. reflexivity. Qed.
imports: Recdef NArith GeoCoq.Utils.sets