Changeset 697 for src/utilities/binary/positive.ma
 Timestamp:
 Mar 18, 2011, 1:28:33 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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).
Note: See TracChangeset
for help on using the changeset viewer.