Ignore:
Timestamp:
Nov 12, 2010, 11:51:18 AM (10 years ago)
Author:
mulligan
Message:

Changes from this morning: Bool / Prop division = nightmare.

File:
1 edited

Legend:

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

    r232 r233  
    197197nqed.
    198198
     199nlemma succ_plus_succ_zero:
     200  ∀n: Nat.
     201    S n = plus n (S Z).
     202  #n.
     203  nelim n.
     204  //.
     205  #N H.
     206  //.
     207nqed.
     208
    199209nlemma plus_symmetrical:
    200210  ∀m, n: Nat.
     
    238248  #N H.
    239249  nnormalize.
    240   napplyS plus_symmetrical.
     250  //.
    241251nqed.
    242252
     
    269279  #N H.
    270280  nnormalize.
    271   napplyS succ_plus.
     281  //.
    272282nqed.
    273283
Note: See TracChangeset for help on using the changeset viewer.