3 files changed, 23 insertions, 0 deletions
diff --git a/coq/ex/mult1.v b/coq/ex/mult1.v
new file mode 100644
index 00000000..7b681782
--- /dev/null
+++ b/coq/ex/mult1.v
@@ -0,0 +1,8 @@
+
+Require Import Arith.
+
+Definition foo:nat := 1%nat.
+
+
+
+
diff --git a/coq/ex/mult2.v b/coq/ex/mult2.v
new file mode 100644
index 00000000..997beefd
--- /dev/null
+++ b/coq/ex/mult2.v
@@ -0,0 +1,7 @@
+
+
+Require Import mult1.
+
+Definition bar:bool := if le_lt_dec foo 0 then true else false.
+
+
diff --git a/coq/ex/mult3.v b/coq/ex/mult3.v
new file mode 100644
index 00000000..d624f339
--- /dev/null
+++ b/coq/ex/mult3.v
@@ -0,0 +1,8 @@
+
+
+Require Import mult2.
+
+Definition foobar := if bar then foo else 2.
+
+
+