diff options
| -rw-r--r-- | coq/ex/mult2.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/coq/ex/mult2.v b/coq/ex/mult2.v index 997beefd..81dede72 100644 --- a/coq/ex/mult2.v +++ b/coq/ex/mult2.v @@ -1,7 +1,5 @@ - - -Require Import mult1. - +Require Import Arith. +Require mult1. Definition bar:bool := if le_lt_dec foo 0 then true else false. |