# HG changeset patch
# User desharna
# Date 1665579024 -7200
# Node ID a627d67434db62900414486a03b4e9b410a4341a
# Parent  5ea1f8bfb795aea0291f1bb2d15d4f2cbe46f46d
added lemma wfP_pfsubset

diff -r 5ea1f8bfb795 -r a627d67434db NEWS
--- a/NEWS	Wed Oct 12 14:37:03 2022 +0200
+++ b/NEWS	Wed Oct 12 14:50:24 2022 +0200
@@ -30,6 +30,9 @@
       wfP_if_convertible_to_wfP
       wf_if_convertible_to_wf
 
+* Theory "HOL-Library.FSet":
+  - Added lemma wfP_pfsubset.
+
 
 New in Isabelle2022 (October 2022)
 ----------------------------------
diff -r 5ea1f8bfb795 -r a627d67434db src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Oct 12 14:37:03 2022 +0200
+++ b/src/HOL/Library/FSet.thy	Wed Oct 12 14:50:24 2022 +0200
@@ -745,6 +745,15 @@
 end
 
 
+subsubsection \<open>@{term fsubset}\<close>
+
+lemma wfP_pfsubset: "wfP (|\<subset>|)"
+proof (rule wfP_if_convertible_to_nat)
+  show "\<And>x y. x |\<subset>| y \<Longrightarrow> fcard x < fcard y"
+    by (rule pfsubset_fcard_mono)
+qed
+
+
 subsubsection \<open>Group operations\<close>
 
 locale comm_monoid_fset = comm_monoid