Changeset 891 for src/utilities/extralib.ma
 Timestamp:
 Jun 7, 2011, 4:53:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r882 r891 119 119 120 120 lemma Zmax_l: ∀x,y. x ≤ Zmax x y. 121 #x #y whd in ⊢ (??%) ; lapply (Z_compare_to_Prop x y); cases (Z_compare x y);122 /3/ ; cases x; /3/;qed.121 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y) 122 /3/ whd in ⊢ (% → ??%) /3/ qed. 123 123 124 124 lemma Zmax_r: ∀x,y. y ≤ Zmax x y. 125 #x #y whd in ⊢ (??%) ; lapply (Z_compare_to_Prop x y); cases (Z_compare x y);126 cases x; /3/;qed.125 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y) 126 whd in ⊢ (% → ??%) /3/ qed. 127 127 128 128 theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. … … 327 327 ∀A:Type[0]. ∀l1,l2:list A. 328 328 l1 @ l2 = [] → l1 = [] ∧ l2 = []. 329 #A #l1 #l2 cases l1 ;330 [ cases l2 ;329 #A #l1 #l2 cases l1 330 [ cases l2 331 331 [ /2/ 332  #h #t #H destruct;333 ] 334  cases l2 ;335 [ normalize ; #h #t #H destruct;336  normalize ; #h1 #t1 #h2 #h3 #H destruct;332  normalize #h #t #H destruct 333 ] 334  cases l2 335 [ normalize #h #t #H destruct 336  normalize #h1 #t1 #h2 #h3 #H destruct 337 337 ] 338 338 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.