Inductive day :=
| Monday
| Tuesday
| Wednesday
| Thursday
| Friday
| Saturday
| Sunday.

About day.

About Friday.

Definition next_day (d : day) : day :=
  match d with
  | Monday => Tuesday
  | Tuesday => Wednesday
  | Wednesday => Thursday
  | Thursday => Friday
  | Friday => Saturday
  | Saturday => Sunday
  | Sunday => Monday
  end.

Eval compute in next_day Tuesday.
Eval compute in next_day (next_day Tuesday).

Theorem next_day_monday : next_day Monday = Tuesday.
Proof.
  reflexivity.
Qed.

Definition previous_day (d : day) : day :=
  match d with
  | Monday => Sunday
  | Tuesday => Monday
  | Wednesday => Tuesday
  | Thursday => Wednesday
  | Friday => Thursday
  | Saturday => Friday
  | Sunday => Saturday
  end.

Theorem previous_next_day : forall d, previous_day (next_day d) = d.
Proof.
  intros d; destruct d; reflexivity.
Qed.

Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S x => S (plus x m)
end.

Theorem S_plus_one n : S n = plus n 1.
Proof.
  induction n as [|x IHx].
  - simpl. reflexivity.
  - simpl. rewrite IHx. reflexivity.
Qed.

Print "+".

Theorem add_com n m : n + m = m + n.
Proof.
  revert m.
  induction n as [|n IHn].
  - intros m.
    simpl.
    induction m as [|m IHm].
    + simpl. trivial.
    + simpl. rewrite <- IHm. reflexivity.
  - intros m.
    induction m as [|m IHm].
    + simpl.
      rewrite IHn. simpl. reflexivity.
    + simpl.
      rewrite IHn.
      simpl.
      rewrite <- IHm.
      simpl.
      rewrite IHn.
      reflexivity.
Qed.

Theorem add_com' n m : n + m = m + n.
Proof.
  revert m.
  induction n; induction m; auto.
  simpl; rewrite IHn; simpl; rewrite <- IHm; simpl; auto.
Qed.

Require Import Coq.micromega.Lia.

Theorem add_com'' n m : n + m = m + n.
Proof. lia. Qed.

Theorem thm : forall x y, x < y -> (x + y) - 2 * x < 2 * y.
Proof. lia. Qed.