Ignore:
Timestamp:
Dec 2, 2010, 2:03:48 PM (10 years ago)
Author:
mulligan
Message:

Resolved conflicts. Added new get_index' which hides the proof obligation of get_index_v. Needed a new lemma to typecheck it.

File:
1 edited

Legend:

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

    r357 r363  
    653653  P (greater_than_b m n).
    654654 #m n; napply less_than_b_elim.
     655nqed.
     656
     657nlemma less_than_or_equal_plus:
     658  ∀n,m: Nat.
     659    n ≤ n + m.
     660  #n m.
     661  nelim n.
     662  //.
     663  #N H.
     664  napply (less_than_or_equal_monotone).
     665  /2/.
    655666nqed.
    656667
Note: See TracChangeset for help on using the changeset viewer.