Ci siamo quasi

[helm.git] / matita / matita / contribs / lambda_delta / ground_2 / arith.ma

diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
index 39d28c959182d17c31fa4a851751928c3fc12b8d..c65a47bcc70b31c7649709157b5e7ac81493c280 100644 (file)
--- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "arithmetics/nat.ma".
-include "Ground_2/star.ma".
+include "ground_2/star.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 
@@ -53,15 +53,15 @@ lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
 #m #Hm * #H /2 width=1/ /3 width=1/
 qed-.
 
-lemma lt_refl_false: ∀n. n < n → False.
+lemma lt_refl_false: ∀n. n < n → ⊥.
 #n #H elim (lt_to_not_eq … H) -H /2 width=1/
 qed-.
 
-lemma lt_zero_false: ∀n. n < 0 → False.
+lemma lt_zero_false: ∀n. n < 0 → ⊥.
 #n #H elim (lt_to_not_le … H) -H /2 width=1/
 qed-.
 
-lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
+lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
 #x #y #H elim (decidable_lt x y) /2 width=1/
 #Hxy elim (H Hxy)
 qed-.