small proofs of the "override" properties of max(a, b) on ℕ

Max_override.v

Require Import Arith.

Lemma max_override_right : forall (n m p : nat), (n >= m) -> max n (max m p) = max n p.
Proof.
  intros n m p ge_n_m.

  inversion ge_n_m ; rewrite Nat.max_assoc.
  - rewrite Nat.max_id.
    reflexivity.
  - rewrite H0.
    rewrite (Nat.max_l n m ge_n_m).
    reflexivity.
Qed.

Lemma max_override_left : forall (n m p : nat), (m <= p) -> max (max n m) p = max n p.
Proof.
  intros n m p le_m_p.

  inversion le_m_p ; rewrite <- Nat.max_assoc.
  - rewrite Nat.max_id.
    reflexivity.
  - rewrite H0.
    rewrite (Nat.max_r m p le_m_p).
    reflexivity.
Qed.