(* week-07_the-ring-tactic.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 05 Jun 2025 *)

(* ********** *)

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

Require Import Arith Bool.

(* ********** *)

Lemma twice_S :
  forall n : nat,
    2 * S n = S (S (2 * n)).
Proof.
  intro n.
  ring.
Qed.

(* ********** *)

Proposition binomial_expansion_2 :
  forall x y : nat,
    (x + y) * (x + y) = x * x + 2 * (x * y) + y * y.
Proof.
  intros x y.
  ring.
Qed.

(* ********** *)

(* end of week-07_the-ring-tactic.v *)