a smaller example to be copy-pasted in the tutorial page

CPGE_2025/web_stub.v

+
+From Coq Require Import ZArith Lia.
+
+Open Scope Z_scope.
+
+Definition inspect {A} (x : A) := 
+  exist (fun y => x = y) x eq_refl.
+
+Notation " v 'eqn' ':' p " := (exist _ v p)
+  (only parsing, at level 20).
+
+Open Scope Z_scope.
+
+Equations sumz (x : Z) : Z by wf (Z.abs_nat x) lt :=
+  sumz x with  inspect (x <=? 0) :=
+  { | true eqn : _ => 0;
+    | (exist _ false p) => x + sumz (x - 1)}.
+Next Obligation.
+lia.
+Qed.
+
+Lemma sumz_eq_wrong (x : Z) : 
+  sumz x = x * (x + 1) / 2.
+Proof.
+funelim (sumz x).
+Abort.
+
+Lemma sumz_eq (x : Z) : 0 <= x -> sumz x = x * (x + 1) / 2.
+funelim (sumz x).
+- intros xge0.
+  assert (xis0 : x = 0) by lia.
+  rewrite xis0.
+  easy.
+- assert (ind_germ : 0 <= x - 1) by lia.
+  intros _.
+  assert (ind : sumz (x - 1) = (x - 1) * (x - 1 + 1) / 2).
+    apply H.
+    easy.
+  rewrite ind.
+  replace (x - 1 + 1) with x by ring.
+  replace (x * (x + 1)) with ((x - 1) * x + x * 2) by ring.
+  rewrite Z.div_add.
+    ring.
+  easy.
+Qed.