Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Theorem mult_plus_one : forall n m : nat,
- m * (S n) = m + m * n.
- Proof.
- intros m n.
- induction n as [| n'].
- simpl.
- reflexivity.
- simpl.
- rewrite -> IHn'.
- rewrite -> plus_swap.
- reflexivity.
- Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement