English
If l2 is a subpermutation of l1, then for any predicate p, countP p (l1 \\ l2) equals countP p l1 minus countP p l2.
Русский
Если l2 является частичной перестановкой l1, то для любого предиката p число истин p на l1\\l2 равно разности счётов p на l1 и l2.
LaTeX
$$$l_2\\ Subperm\\ l_1\\ \\Rightarrow\\ \\forall p:\\alpha\\to Bool,\\ countP\\ p\\ (l_1\\ diff\\ l_2) = countP\\ p\\ l_1 - countP\\ p\\ l_2$$$
Lean4
theorem countP_diff (hl : l₂ <+~ l₁) (p : α → Bool) : countP p (l₁.diff l₂) = countP p l₁ - countP p l₂ :=
by
refine (Nat.sub_eq_of_eq_add ?_).symm
rw [← countP_append]
exact ((subperm_append_diff_self_of_count_le <| subperm_ext_iff.1 hl).symm.trans perm_append_comm).countP_eq _
