Ignore:
Timestamp:
Feb 15, 2013, 11:27:59 AM (8 years ago)
Author:
campbell
Message:

Clean up from recent commits.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extranat.ma

    r2286 r2670  
    6161[ @H
    6262| @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) //
     63] qed.
     64
     65lemma max_O_n : ∀n. max O n = n.
     66* //
     67qed.
     68
     69lemma max_n_O : ∀n. max n O = n.
     70* //
     71qed.
     72
     73lemma associative_max : associative nat max.
     74#n #m #o normalize
     75@(leb_elim n m)
     76[ normalize @(leb_elim m o) normalize #H1 #H2
     77  [ >(le_to_leb_true n o) /2/
     78  | >(le_to_leb_true n m) //
     79  ]
     80| normalize @(leb_elim m o) normalize #H1 #H2
     81  [ %
     82  | >(not_le_to_leb_false … H2)
     83    >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/
     84  ]
    6385] qed.
    6486
Note: See TracChangeset for help on using the changeset viewer.