## use Qp inequality instead of frac validity for lemma statements

Many lemma statements use `✓ q`

instead of `(q ≤ 1)%Qp`

to express validity of a fraction. There was no `≤`

on `Qp`

before Robbert's recent changes, so this makes sense historically. It is also true that `✓ q`

is shorter, but it is rather cryptic, and usually the user will think in terms of inequalities and not validity of fractions.

So with this MR I propose we change all these lemma statements to use inequality instead. I used `rg '✓[^↔→⊢]*%Qp|✓[ {}n]*[qp]'`

to find the lemmas that would need changing from this; I hope I did not miss any. The one thing I did not change is the definition of validity of `view`

, but I am happy to also change that if people prefer.

We should also avoid using `⋅`

for `Qp`

addition and `≼`

for `≤`

, but I could not find any instances of that.