Task

Use these 2 theorems to prove a theorem:

Keywords: pattern matching, goal, tactic, rewrite

What is goal?

goal is the theorem we want to prove in current context, like in this example

forall p : nat, p × 1 = p

first, introduce a parameter p

Coq automatically match the p with variable in goal

rewrite has 2 types: -> and <-

for first case you can consider it as expand from LHS(Left Hand Side) to RHS according to the rewrited theorem.

p * S O = p * O + p (rewrite theorem mult_n_Sm with n = p and m = O <-)
        = O + p (rewrite theorem mult_n_O with n = p <-)
        = p