Prop?

[sven--]

Trying to prove this, but the material have not mentioned about "Prop" type before.
(from MoreCoq.v)

Theorem double_induction: forall (P : nat -> nat -> Prop),
P 0 0 ->
(forall m, P m 0 -> P (S m) 0) ->
(forall n, P 0 n -> P 0 (S n)) ->
(forall m n, P m n -> P (S m) (S n)) ->
forall m n, P m n.

[sven--]

Can I reduce the following expression?
P 0 0 -> P 0 0

[sven--]

Is there any way to use above theorem to solve this problem?
(** **** Exercise: 3 stars (beq_nat_sym) *)
Theorem beq_nat_sym : forall (n m : nat),
beq_nat n m = beq_nat m n.

Below is what I tried ->
----------#####--------------
Definition beq_nat_sym_def (n m : nat) : Prop :=
beq_nat n m = beq_nat m n.
Theorem beq_nat_sym_thm : forall (n m : nat), (beq_nat_sym_def n m).
Proof.
Check double_induction.
intros n m.
rewrite double_induction.
----------#####--------------

Didn't work and I had to find another sol.

[jeehoonkang]

Wonder if this issue was resolved.