Some integrations from CerCo. In particular:

[helm.git] / matita / matita / lib / arithmetics / nat.ma

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 56482a0428e6e434a880d23d9f4dcd9f042e0c9c..266f01ef8c63d072e7c3e9d34657295402a7489c 100644 (file)
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -700,10 +700,10 @@ theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
 
 (* min e max *)
 definition min: nat →nat →nat ≝
-λn.λm. if_then_else ? (leb n m) n m.
+λn.λm. if leb n m then n else m.
 
 definition max: nat →nat →nat ≝
-λn.λm. if_then_else ? (leb n m) m n.
+λn.λm. if leb n m then m else n.
 
 lemma commutative_min: commutative ? min.
 #n #m normalize @leb_elim