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.