Changeset 1316 for src/utilities/extralib.ma
 Timestamp:
 Oct 7, 2011, 12:26:39 PM (10 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src

Property
svn:mergeinfo
set to
/Deliverables/D3.3/idlookupbranch merged eligible

Property
svn:mergeinfo
set to

src/utilities/extralib.ma
r1260 r1316 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.