"(1 ≤ qmax)%Qp" simplifies to something horrible
I have a (1 ≤ qmax)%Qp
in my goal (with qmax: Qp
), and when I do simpl
, it becomes let 'mk_Qp q _ := qmax in (1 ≤ q)%Qc
.
I have a (1 ≤ qmax)%Qp
in my goal (with qmax: Qp
), and when I do simpl
, it becomes let 'mk_Qp q _ := qmax in (1 ≤ q)%Qc
.