Coq simplification "issue"

Basic.v

Inductive letter : Type := A | B| C | D | E | F.

Inductive modifier : Type := Plus | Natural | Minus.

Inductive grade : Type := Grade (l: letter) (m: modifier).

Inductive comparison: Set :=
| Eq: comparison
| Lt: comparison
| Gt: comparison.

Definition letter_comparison (l1 l2 : letter) : comparison :=
  match l1, l2 with
  | A, A => Eq
  | A, _ => Gt
  | B, A => Lt
  | B, B => Eq
  | B, _ => Gt
  | C, (A | B) => Lt
  | C, C => Eq
  | C, _ => Gt
  | D, (A | B | C) => Lt
  | D, D => Eq
  | D, _ => Gt
  | E, E => Eq
  | E, F => Gt
  | E, _ => Lt
  | F, (A | B | C | D | E) => Lt
  | F, F => Eq

  end.

Theorem letter_comparison_Eq :
  forall l, letter_comparison l l = Eq.
Proof.
  intros [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

Definition modifier_comparison (m1 m2 : modifier) : comparison :=
  match m1, m2 with
  | Plus, Plus => Eq
  | Plus, _ => Gt
  | Natural, Plus => Lt
  | Natural, Natural => Eq
  | Natural, _ => Gt
  | Minus, (Plus | Natural) => Lt
  | Minus, Minus => Eq
  end.

(** I wrote that *)
Definition grade_comparison (g1 g2 : grade) : comparison :=
  match g1, g2 with
  | Grade l1 m1, Grade l2 m2 =>
      match letter_comparison l1 l2 with
      | Eq         => modifier_comparison m1 m2
      | _ as other => other
      end
  end.

Example test_grade_comparison1 :
  (grade_comparison (Grade A Minus) (Grade B Plus)) = Gt.
Proof. simpl. reflexivity. Qed.

Example test_grade_comparison2 :
  (grade_comparison (Grade A Minus) (Grade A Plus)) = Lt.
Proof. simpl. reflexivity. Qed.

Example test_grade_comparison3 :
  (grade_comparison (Grade F Plus) (Grade F Plus)) = Eq.
Proof. simpl. reflexivity. Qed.

Example test_grade_comparison4 :
  (grade_comparison (Grade B Minus) (Grade C Plus)) = Gt.
Proof. simpl. reflexivity. Qed.

(** I wrote that *)
Definition lower_letter (l : letter) : letter :=
  match l with
  | A => B
  | B => C
  | C => D
  | D => E
  | E => F
  | F => F
  end.

(** I wrote that *)
Theorem lower_letter_lowers:
  forall (l : letter),
    letter_comparison F l = Lt ->
    letter_comparison (lower_letter l) l = Lt.
Proof.
  intros [] H.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - rewrite <- H. simpl. reflexivity.
Qed.

(** I wrote that *)
Definition lower_modifier m :=
  match m with
  | Plus => Natural
  | Natural | Minus => Minus
  end.

(** I wrote that *)
Definition lower_grade (g : grade) : grade :=
  match g with
  | Grade F Minus => Grade F Minus
  | Grade l Minus => Grade (lower_letter l) Plus
  | Grade l m => Grade l (lower_modifier m)
  end.

Theorem lower_grade_lowers :
  forall (g : grade),
    grade_comparison (Grade F Minus) g = Lt ->
    grade_comparison (lower_grade g) g = Lt.
Proof.
  intros [] H. destruct m.
  - simpl. cbn.

Most of the code is given to me (source), I've flagged the bit that I wrote myself with a comment.