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.