From 31f07b96505d596751d541d1ee8656bbf8e75147 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hu=E1=BB=B3nh=20Tr=E1=BA=A7n=20Khanh?=
 <qcdz9r6wpcbh59@gmail.com>
Date: Sat, 16 Nov 2024 13:10:51 +0000
Subject: [PATCH] Add DisjointSetUnionCode3.v

---
 _CoqProject                      | 1 +
 theories/DisjointSetUnionCode3.v | 5 +++++
 2 files changed, 6 insertions(+)
 create mode 100644 theories/DisjointSetUnionCode3.v

diff --git a/_CoqProject b/_CoqProject
index 4d0fcb7..6a23506 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -28,5 +28,6 @@ theories/DisjointSetUnion.v
 theories/CountingBits.v
 theories/DisjointSetUnionCode.v
 theories/DisjointSetUnionCode2.v
+theories/DisjointSetUnionCode3.v
 -R generated-coq/ Generated
 generated-coq/DisjointSetUnion.v
diff --git a/theories/DisjointSetUnionCode3.v b/theories/DisjointSetUnionCode3.v
new file mode 100644
index 0000000..8285039
--- /dev/null
+++ b/theories/DisjointSetUnionCode3.v
@@ -0,0 +1,5 @@
+From CoqCP Require Import DisjointSetUnionCode Options.
+From stdpp Require Import numbers list.
+
+Lemma maxScoreIsAttainable : interact state (map (fun x => (0%Z, Z.of_nat x)) (seq 1 99)) = 5049%Z.
+Proof. reflexivity. Qed.