From Coq Require Import Arith List.
From Coq Require Import Lia.
Require Import Ring.

Theorem plus_id_exercise : forall n m o : nat,
    n = m -> m = o -> n + m = m + o.
Proof.
  lia.
Qed.

Theorem add_assoc : forall n m p : nat,
    n + (m + p) = (n + m) + p.
Proof.
  lia.
Qed.

Theorem S_injective : forall (n m : nat),
    S n = S m -> n = m.
Proof.
  congruence.
Qed.

Theorem or_distributes_over_and : forall P Q R : Prop,
    P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
  intuition.
Qed.