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

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?

you can do destruct (factorial (Z.to_nat n)).
• This worked like a charm! Thank you very much. I had never seen destruct used like this, only directly on variables. This is good to know. Commented Apr 14, 2023 at 8:22
• destruct is a very powerful tactic. Don't hesitate to look it up in the doc. I think you could also use destruct factorial, it will have automatically selected the term in your goal on which to perform the case analysis.
• Yep, tried just destruct factorial and that also worked. I'll be sure to check it out in the docs. I'm relatively new to Coq, and I find proofs difficult because often I don't even know which tactic I need, so I'm not sure which one to look up. I'm sure I'll get the hang of it. Commented Apr 14, 2023 at 8:31