Prove $a\leq b$ or $b \leq a$ in Coq I am reading the software foundations for Coq, and one property that I would like to prove is the excluded middle for $\leq$. The definitions are the following
Inductive nat : Type :=
| O
| S (n : nat).


Inductive bool : Type :=
  | true
  | false.

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
end.
Notation "x <=? y" := (leb x y) (at level 70).
Theorem EQEM: forall n m, n <=? m = true \/ n <=? m = false.

The proof is easy but how to implement it in Coq? Since the function is to type bool and terminates, the output is always a bool, and that should complete the proof. Induction seems to lead nowhere, although an infinite descent argument also  concludes the matter trivially, perhaps there is something I missed...

And here are the answers, thank you for the very helpful comments. First, as was pointed out, a regular induction can solve the problem. Some attention must be paid to the order of operations, it is possible to get stuck.
Theorem EQEM: forall n m, n <=? m = true \/ n <=? m = false.
induction n. intros m. destruct m. left. reflexivity.
left. reflexivity. intros m. induction m. right.
reflexivity. specialize (IHn m). simpl. exact IHn.
Qed.

However, the substitution proof works as well.
Theorem LEMB: forall b: bool, b = true \/ b = false.
Proof. destruct b. left. reflexivity. right. reflexivity. Qed.

Theorem EQEM: forall n m, n <=? m = true \/ n <=? m = false.
Proof. pose LEMB as H. intros n m. specialize (H (n <=? m)).
exact H. Qed.

