Changeset 1516 for src/utilities/extralib.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/extralib.ma
r1515 r1516 120 120 121 121 lemma Zmax_l: ∀x,y. x ≤ Zmax x y. 122 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)122 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y) 123 123 /3/ qed. 124 124 125 125 lemma Zmax_r: ∀x,y. y ≤ Zmax x y. 126 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)127 whd in ⊢ (% → ??%) /3/ qed.126 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y) 127 whd in ⊢ (% → ??%); /3/ qed. 128 128 129 129 theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. … … 224 224 225 225 theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m. 226 #n #m #H % #H' >(Zle_to_Zleb_true … H') in H #H destruct;226 #n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct; 227 227 qed. 228 228 … … 244 244 245 245 theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m. 246 #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H #H destruct;246 #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct; 247 247 qed. 248 248 … … 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 % [ normalize /3 / | *: normalize /2/ ] @plt_pos542 #lt #e destruct % [ normalize /3 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @plt_pos 543 543 [ 1,3,5,7: @double_lt1 /2/; 544 544 | 2,4: @double_lt3 /2/; … … 583 583 cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ] 584 584 cases md'; [ 2,4: #md'' ] #DIVIDE normalize; 585 >DIV in ⊢ (% → ?) #H #lt destruct;585 >DIV in ⊢ (% → ?); #H #lt destruct; 586 586 [ lapply (plus_to_minus … e0); 587 587 >(commutative_times …) >(commutative_times dv'' …)
Note: See TracChangeset
for help on using the changeset viewer.