Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (9 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extranat.ma

    r1515 r1516  
    2424#n elim n
    2525[ @refl
    26 | #m #IH whd in ⊢ (??%?) > IH @refl
     26| #m #IH whd in ⊢ (??%?); >IH @refl
    2727] qed.
    2828
     
    3030#n #m elim n
    3131[ //
    32 | #n' #IH whd in ⊢ (??%?) > IH @refl
     32| #n' #IH whd in ⊢ (??%?); >IH @refl
    3333] qed.
    3434
     
    3636#n #m elim m
    3737[ //
    38 | #m' #IH whd in ⊢ (??%?) > IH @refl
     38| #m' #IH whd in ⊢ (??%?); >IH @refl
    3939] qed.
    4040
     
    5252
    5353lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
    54 #m #n #o #H whd in ⊢ (??%) @leb_elim #H'
     54#m #n #o #H whd in ⊢ (??%); @leb_elim #H'
    5555[ @(transitive_le ? m ? H H')
    5656| @H
     
    5858
    5959lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n.
    60 #m #n #o #H whd in ⊢ (??%) @leb_elim #H'
     60#m #n #o #H whd in ⊢ (??%); @leb_elim #H'
    6161[ @H
    6262| @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) //
Note: See TracChangeset for help on using the changeset viewer.