Changeset 697 for src/utilities
 Timestamp:
 Mar 18, 2011, 1:28:33 PM (10 years ago)
 Location:
 src/utilities
 Files:

 4 edited
 1 moved
Legend:
 Unmodified
 Added
 Removed

src/utilities/Coqlib.ma
r695 r697 18 18 library. *) 19 19 20 include " binary/Z.ma".20 include "utilities/binary/Z.ma". 21 21 include "basics/types.ma". 22 22 include "basics/list.ma". 23 23 24 include " extralib.ma".24 include "utilities/extralib.ma". 25 25 26 26 (* 
src/utilities/binary/Z.ma
r487 r697 17 17 18 18 (*include "arithmetics/compare.ma".*) 19 include " binary/positive.ma".19 include "utilities/binary/positive.ma". 20 20 21 21 inductive Z : Type[0] ≝ 
src/utilities/binary/positive.ma
r487 r697 17 17 include "basics/logic.ma". 18 18 include "arithmetics/nat.ma". 19 include " oldlib/eq.ma".19 include "utilities/oldlib/eq.ma". 20 20 21 21 (* arithmetics/comparison.ma > *) … … 365 365 366 366 theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m. 367 /3/;qed.367 #n #m @not_to_not @le_S_S_to_le qed. 368 368 369 369 theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m. 370 /3/;qed.370 #n #m @not_to_not /2/ qed. 371 371 372 372 theorem decidable_le: ∀n,m:Pos. decidable (n≤m). 
src/utilities/extralib.ma
r695 r697 16 16 include "basics/list.ma". 17 17 include "basics/logic.ma". 18 include " binary/Z.ma".19 include " binary/positive.ma".18 include "utilities/binary/Z.ma". 19 include "utilities/binary/positive.ma". 20 20 21 21 lemma eq_rect_Type0_r:
Note: See TracChangeset
for help on using the changeset viewer.