Changeset 1811


Ignore:
Timestamp:
Mar 8, 2012, 11:37:42 AM (7 years ago)
Author:
boender
Message:
  • corrected definition of geb
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1602 r1811  
    1919definition geb ≝
    2020  λm, n: nat.
    21     ltb n m.
     21    leb n m.
    2222
    2323definition gtb ≝
     
    228228  λproof   : 0 < | the_list |.
    229229    nth_safe elt_type (|the_list| - 1) the_list ?.
    230   normalize /2/
     230  normalize /2 by lt_plus_to_minus/
    231231qed.
    232232
     
    743743 #m #n #H
    744744 elim H
    745  /2/
     745 /2 by le_n, le_S/
    746746qed.
    747747
     
    758758   normalize
    759759   [ #H
    760      /2/
    761    | /3/
     760     /2 by /
     761   | /3 by not_le_to_not_le_S_S/
    762762   ]
    763763 ]
     
    775775 [ #H
    776776   destruct
    777  | #n #H lapply (H1 … H) /2/
     777 | #n #H lapply (H1 … H) /2 by le_S_S/
    778778 ]
    779779qed.
     
    787787 lapply (less_than_or_equal_b_complete m n)
    788788 cases (leb m n)
    789  /3/
     789 /3 by /
    790790qed.
    791791
Note: See TracChangeset for help on using the changeset viewer.