 Timestamp:
 Mar 8, 2012, 11:37:42 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1602 r1811 19 19 definition geb ≝ 20 20 λm, n: nat. 21 l tb n m.21 leb n m. 22 22 23 23 definition gtb ≝ … … 228 228 λproof : 0 <  the_list . 229 229 nth_safe elt_type (the_list  1) the_list ?. 230 normalize /2 /230 normalize /2 by lt_plus_to_minus/ 231 231 qed. 232 232 … … 743 743 #m #n #H 744 744 elim H 745 /2 /745 /2 by le_n, le_S/ 746 746 qed. 747 747 … … 758 758 normalize 759 759 [ #H 760 /2 /761  /3 /760 /2 by / 761  /3 by not_le_to_not_le_S_S/ 762 762 ] 763 763 ] … … 775 775 [ #H 776 776 destruct 777  #n #H lapply (H1 … H) /2 /777  #n #H lapply (H1 … H) /2 by le_S_S/ 778 778 ] 779 779 qed. … … 787 787 lapply (less_than_or_equal_b_complete m n) 788 788 cases (leb m n) 789 /3 /789 /3 by / 790 790 qed. 791 791
Note: See TracChangeset
for help on using the changeset viewer.