Fix one Lean misformalisation #217

The hypotheses were contradictory without the missing positivity guard as the following succeeds without the change included here: ``` exfalso have : IsQualifying S := hS.1 rw [IsQualifying_def] at this obtain ⟨h₁, h₂, h₃, h₄⟩ := this have : -7 ∈ S := h₃ (-7) (h₄ 2 h₂) replace this : 0 < -7 := h₁ _ this linarith ``` This was previously "fixed" in c4512ca but unfortunately an error remained.