Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (7 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extranat.ma

    r2824 r3081  
    1313    ]
    1414].
     15
     16lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.
     17#x0 elim x0
     18[ #y %{y} %2 %
     19| #x #IH *
     20  [ %{(S x)} %1 %
     21  | #y cases (IH y) #z *
     22    [ #H %{z} %1 >H //
     23    | #H %{z} %2 >H //
     24    ]
     25  ]
     26] qed.
    1527
    1628inductive nat_compared : nat → nat → Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.