Proof that "if m <= n then max(m, n) = n" in Coq

Question

Yesterday I asked a question here about a proof in Coq and the answer helped me a lot, I was able to solve many exercises alone and discover new features. Today I have another exercise, which states that For all m, n, if m <= n then max(m,n) = n. I tried to do induction after m, but I got stuck. Any help would be appreciated!

Fixpoint max (m n : Nat) : Nat :=
  match m with
  | O => n
  | S m' => match n with
            | O => m
            | S n' => S (max m' n')
            end
  end.

Fixpoint le_Nat (m n : Nat) : bool :=
  match m with 
  | O => true
  | S m' => match n with 
            | O => false
            | S n' => (le_Nat m' n')
            end
  end.

Lemma:

Lemma le_max_true :
  forall m n,
    le_Nat m n = true ->
    max m n = n.
Proof.
    ...
Qed.

Answer 1

Let's consider the 4th sub-goal.

1 goal (ID 39)
  
  m : nat
  IHm : forall n : nat, le_nat m n = true -> max m n = n
  n : nat
  ============================
  le_nat m n = true -> S (max m n) = S n

rewrite IHm is able to replace (max m N) with N(for any N), under the condition le_nat m N = true.

By an intro H, you push an hypothesis of type le_nat m n = true into the context. Then your rewrite IHm generates two (trivial) sub-goals.

In short, in order to solve the 4th sub-goal, you may start with intro H; rewrite IHm.

If you forget the intro H, you get an unsolvable goal:

  m : Nat
  IHm : forall n : Nat, le_Nat m n = true -> max m n = n
  n : Nat
  ============================
  le_Nat m n = true