t.v

Goal  forall (A : Prop), A -> A.
intros.
exact H.
Qed.

Require Import Arith.
Theorem plus_comm: forall (n m : nat), (n + m) = m + n.
intros.
induction m.
simpl.
induction n.
simpl.
reflexivity.
simpl.
rewrite IHn.
reflexivity.

simpl.
rewrite <- plus_n_Sm.
f_equal.
exact IHm.
Qed.

Goal forall (n m: nat), (n*m) = (m*n).
intros.
induction n.
simpl.
rewrite <- mult_n_O.
reflexivity.

rewrite <- mult_n_Sm.
simpl.
rewrite plus_comm.
f_equal.
exact IHn.
Qed.