calc zlengthOfSet (X \ Cond ∪ Res)
    ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res := by
        have := @Finset.sum_union_inter _ _ (X \ Cond) Res zlengthOf _ _
        have : zlengthOfSet (X \ Cond ∩ Res) ≥ 0 := zlengthOfSet.pos
        simp_all
        linarith
  _ = zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res := by
        simp only [zlengthOfSet]
        rw [Finset.sum_sdiff_eq_sub precondProof]
  _ < zlengthOfSet X := by
        have : zlengthOfSet Res < zlengthOfSet Cond := by
          rw [← zlen_iff]
          exact hyp
        linarith
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) < zlengthOfSet X
no goals