Simple proofs using case analysis in Coq taken from By Case Analysis section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html

caseAnalysis.v

(* taken from By Case Analysis section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Fixpoint beq_nat (n m : nat) : bool :=
  match n, m with
  | O, O       => true
  | O, _       => false
  | S _, O     => false
  | S n', S m' => beq_nat n' m'
  end.

Theorem plus_1_neq_0 : forall n : nat,
  beq_nat (n + 1) 0 = false.

Proof.
  intros.
  destruct n as [| n'].
  - reflexivity.
  - reflexivity.
Qed.

Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Proof.
  intros b.
  destruct b.
  - reflexivity.
  - reflexivity.
Qed.

Theorem andb_commutative : forall a b : bool,
  andb a b = andb b a.
Proof.
  intros a b.
  destruct a.
  - destruct b.
   + reflexivity.
   + reflexivity.
  - destruct b.
   + reflexivity.
   + reflexivity.
Qed.

Theorem andb_true_elim2 : forall a b : bool,
  andb a b = true -> b = true.
Proof.
  intros [] [].
  - reflexivity.
  - tauto.
  - reflexivity.
  - tauto.
Qed.

Theorem zero_nbeq_plus_1 : forall n : nat,
  beq_nat 0 (n + 1) = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity.
Qed.