How do I prove an expression in Coq that involves pattern matching?

Question

I'm working on a proof in Coq and my proof state is as follows:

n: Z
H: 1 < n
1/1
match factorial (Z.to_nat n) with
| 0 => 0
| Z.pos y' => Z.pos y'
| Z.neg y' => Z.neg y'
end = factorial (Z.to_nat n)

My factorial function, in turn, is:

Fixpoint factorial (n : nat) : Z :=
  match n with
  | O => 1
  | S p => Z.of_nat n * factorial p
  end.

I am not sure which tactics to use to complete this proof. It seems pretty straightforward, but nothing seems to be working to get rid of the pattern matching expression. Can anybody help me?

Answer 1

you can do destruct (factorial (Z.to_nat n)).