Ignore:
Timestamp:
Aug 4, 2011, 1:55:53 PM (9 years ago)
Author:
campbell
Message:

Tidy up branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/utilities/extralib.ma

    r891 r1102  
    1616include "basics/list.ma".
    1717include "basics/logic.ma".
     18include "utilities/pair.ma".
    1819include "utilities/binary/Z.ma".
    1920include "utilities/binary/positive.ma".
     
    516517lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
    517518/2/; qed.
    518 
    519 lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
    520 #A #B #a1 #a2 #b1 #b2 #H destruct //
    521 qed.
    522 
    523 lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
    524 #A #B #a1 #a2 #b1 #b2 #H destruct //
    525 qed.
    526519
    527520theorem divide_ok : ∀m,n,dv,md.
Note: See TracChangeset for help on using the changeset viewer.