Coq basic operators

(* adding two natural numbers *)
Fixpoint nat_add (m n: nat): nat :=
  match m with
  | O => n
  | S m' => S (nat_add m' n)
  end.

(* multiplying two natural numbers *)
Fixpoint nat_mul (m n: nat): nat :=
  match m with
  | O => O
  | S m' => nat_add n (nat_mul m' n)
  end.

(* power of two natural numbers *)
Fixpoint nat_exp (base power: nat): nat :=
  match power with
  | O => S O
  | S power => nat_mul base (nat_exp base power)
  end.

Theorem test_nat_add: (nat_add 5 6) = 11.
Proof. reflexivity. Qed.

Theorem test_nat_mul: (nat_mul 5 6) = 30.
Proof. reflexivity. Qed.

Theorem test_nat_exp: (nat_exp 2 3) = 8.
Proof. reflexivity. Qed.

(* GROUP THEORY ?? *)

Theorem test_0: forall n: nat, nat_add 0 n = n.
Proof. reflexivity. Qed.
Theorem test_1: forall n: nat, nat_mul 0 n = 0.
Proof. reflexivity. Qed.