Changeset 1517
 Timestamp:
 Nov 19, 2011, 12:38:36 AM (8 years ago)
 Location:
 src/utilities/binary
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/binary/Z.ma
r891 r1517 237 237 #m cases z 238 238 [// 239 #p applytransitive_lt (* XXX: auto??? *)239 #p @transitive_lt (* XXX: auto??? *) 240 240 //] 241 241 #m #Hl cases Hl] … … 249 249 #m cases z 250 250 [1,2:// 251 #p #Hl #Hr apply(transitive_lt … Hr Hl)]251 #p #Hl #Hr @(transitive_lt … Hr Hl)] 252 252 ] 253 253 ] … … 463 463 [// 464 464 // 465 #q whd in ⊢ (??%%) >pos_compare_n_m_m_n465 #q whd in ⊢ (??%%); >pos_compare_n_m_m_n 466 466 cases (pos_compare q p);//] 467 467 #p cases y 468 468 [//; 469 #q whd in ⊢ (??%%) >pos_compare_n_m_m_n469 #q whd in ⊢ (??%%); >pos_compare_n_m_m_n 470 470 cases (pos_compare q p);// 471 471 normalize;//] … … 503 503 ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)). 504 504 #n #m 505 whd in ⊢ (??%%) 505 whd in ⊢ (??%%); 506 506 <(pos_compare_S_S …) 507 507 >(minus_S_S …) … … 522 522 [ //; 523 523  #m' >Zpred_pos_succ 524 change in ⊢ (??(??%)?) with (Zsucc (pos m'))524 change in ⊢ (??(??%)?); with (Zsucc (pos m')) 525 525 <Zpred_Zplus_neg_O >Zpred_Zsucc @refl 526  #m' whd in ⊢ (??%%) >pos_compare_S_one normalize;526  #m' whd in ⊢ (??%%); >pos_compare_S_one normalize; 527 527 >partial_minus_S_one normalize; >pos_nonzero 528 528 <pred_succ_n // 529  #m' #n' whd in ⊢ (??%%) <pos_compare_S_S529  #m' #n' whd in ⊢ (??%%); <pos_compare_S_S 530 530 >minus_S_S 531 531 >minus_S_S normalize … … 601 601 602 602 lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m. 603 #n #m whd in ⊢ (??%%) <pos_compare_S_S603 #n #m whd in ⊢ (??%%); <pos_compare_S_S 604 604 >minus_S_S >minus_S_S 605 605 //; qed. … … 676 676 #x #y cases x 677 677 [cases y;// 678 *:#n cases y;//;#m whd in ⊢ (??(?%)%) @pos_compare_elim normalize;//]678 *:#n cases y;//;#m whd in ⊢ (??(?%)%); @pos_compare_elim normalize;//] 679 679 qed. 680 680 … … 686 686 #x cases x 687 687 [// 688 *:#n whd in ⊢ (??%?) >pos_compare_n_n //]688 *:#n whd in ⊢ (??%?); >pos_compare_n_n //] 689 689 qed. 690 690 
src/utilities/binary/positive.ma
r1515 r1517 213 213 #n elim n; normalize; 214 214 [ // 215  2,3: #n' #IH #m cases m; /3 /;216 normalize; cases n' ; //;215  2,3: #n' #IH #m cases m; /3 by eq_f, sym_eq/ 216 normalize; cases n' // 217 217 ] qed. 218 218 … … 284 284 @pos_elim 285 285 [ // 286  #n #IH #m <(times_succn_m …) <(times_succn_m …) /3 /;286  #n #IH #m <(times_succn_m …) <(times_succn_m …) /3 by succ_injective, trans_eq/ 287 287 ] qed. 288 288 … … 449 449 450 450 theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m. 451 @pos_elim2 /4 /;451 @pos_elim2 /4 by le_n_one_to_eq, monotonic_pred, eq_f, sym_eq/ 452 452 qed. 453 453 … … 913 913 #n #m #p #lep 914 914 @transitive_le 915 [ applyle_plus_minus_m_m915 [@le_plus_minus_m_m 916 916 @monotonic_le_plus_l //; 917 917 ] … … 1138 1138 1139 1139 theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m. 1140 (* sic1141 #n #m #H elim H1142 [//1143 /2/] *)1144 1140 /2/; qed. 1145 1141 1146 1142 lemma cmp_nat: ∀n,m:Pos.cmp_cases n m. 1147 1143 #n #m lapply (pos_compare_to_Prop n m) 1148 cases (pos_compare n m);normalize; /3 /;1144 cases (pos_compare n m);normalize; /3 by lt_times_n_to_lt_l, le_n, cmp_le, cmp_gt, lt_to_le/ 1149 1145 qed. 1150 1146
Note: See TracChangeset
for help on using the changeset viewer.