1 files changed, 7 insertions, 0 deletions
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.
+
+