Changeset 1337


Ignore:
Timestamp:
Oct 10, 2011, 4:03:19 PM (8 years ago)
Author:
sacerdot
Message:

Automation is now stronger.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1316 r1337  
    121121lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    122122#x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
    123 /3/ whd in ⊢ (% → ??%) /3/ qed.
     123/3/ qed.
    124124
    125125lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
Note: See TracChangeset for help on using the changeset viewer.