I have to prove a goal in the form:
forall x: ordinal_finType m, P x
I am currently in a case where I have Hm: m = 0
in my stack, so this is essentially a forall
over an empty set. How can I proceed in this case?
Using
case => x.
leaves me with
forall i : (x < m)%N, P i
but then of course I cannot use rewrite Hm
as it fails with a dependent type error.
Well you would need to rewrite with you zero hypothesis, actually the proof of emptiness is trivial due to the computational nature of the
<
operator in math-comp.or if you want: