Changeset 1350 for src/utilities
 Timestamp:
 Oct 11, 2011, 2:27:53 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r1338 r1350 522 522 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n. 523 523 #m #n @(pos_cases … n) 524 [ >(divide_by_one m) #dv #md #H destruct /2/524 [ >(divide_by_one m) #dv #md #H destruct normalize /2/ 525 525  #n' elim m; 526 526 [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/ … … 540 540 lapply (partial_minus_to_Prop md'' n); 541 541 cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize 542 #lt #e destruct % [ /3/  *:/2/ ] @plt_pos542 #lt #e destruct % [ normalize /3/  *: normalize /2/ ] @plt_pos 543 543 [ 1,3,5,7: @double_lt1 /2/; 544 544  2,4: @double_lt3 /2/;
Note: See TracChangeset
for help on using the changeset viewer.