Changeset 1102 for Deliverables/D3.3/idlookupbranch/utilities/extralib.ma
 Timestamp:
 Aug 4, 2011, 1:55:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/utilities/extralib.ma
r891 r1102 16 16 include "basics/list.ma". 17 17 include "basics/logic.ma". 18 include "utilities/pair.ma". 18 19 include "utilities/binary/Z.ma". 19 20 include "utilities/binary/positive.ma". … … 516 517 lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m. 517 518 /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.526 519 527 520 theorem divide_ok : ∀m,n,dv,md.
Note: See TracChangeset
for help on using the changeset viewer.