Ignore:
Timestamp:
Nov 23, 2010, 3:50:28 PM (11 years ago)
Author:
mulligan
Message:

Strengthened typings of get_ and set_index in Vector file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Nat.ma

    r260 r261  
    207207nqed.
    208208
     209naxiom less_than_or_equal_injective:
     210  ∀m, n: Nat.
     211    S m ≤ S n → m ≤ n.
     212
    209213(*
    210 nlemma less_than_or_equal_injective:
    211   ∀m, n: Nat.
    212     S m ≤ S n → m ≤ n.
    213   #m n.
    214   nelim m.
    215   #H.
    216   napplyS less_than_or_equal_zero.
    217   #N H H2.
    218   ndestruct.
    219 
    220214nlemma less_than_or_equal_zero_equal_zero:
    221215  ∀m: Nat.
     
    249243  napplyS less_than_or_equal_zero.
    250244  #N H H2.
    251   //.
    252   napplyS H.
    253 
     245  nrewrite > H.
     246  nnormalize.
    254247
    255248nlemma less_than_or_equal_transitive:
     
    262255  #N H H2.
    263256  nnormalize.
    264   #;
    265257*)
    266258
Note: See TracChangeset for help on using the changeset viewer.