Changeset 961 for src/utilities/extranat.ma

Timestamp:

Jun 15, 2011, 4:15:52 PM (10 years ago)

Author:

campbell

Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:

• src/utilities/extranat.ma (modified) (1 diff)

src/utilities/extranat.ma

@@ -19 +19 @@
     ]
 ].
+
+lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n.
+#n elim n
+[ @refl
+| #m #IH whd in ⊢ (??%?) > IH @refl
+] qed.
+
+lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m.
+#n #m elim n
+[ //
+| #n' #IH whd in ⊢ (??%?) > IH @refl
+] qed.
+
+lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m.
+#n #m elim m
+[ //
+| #m' #IH whd in ⊢ (??%?) > IH @refl
+] qed.
 
 lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.