Ignore:
Timestamp:
Mar 18, 2011, 1:28:33 PM (9 years ago)
Author:
campbell
Message:

Merge Clight branch of vectors and friends.
Start making stuff build.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/positive.ma

    r487 r697  
    1717include "basics/logic.ma".
    1818include "arithmetics/nat.ma".
    19 include "oldlib/eq.ma".
     19include "utilities/oldlib/eq.ma".
    2020
    2121(* arithmetics/comparison.ma --> *)
     
    365365
    366366theorem 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.
    368368
    369369theorem 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.
    371371
    372372theorem decidable_le: ∀n,m:Pos. decidable (n≤m).
Note: See TracChangeset for help on using the changeset viewer.