Changeset 3081 for src/utilities/extranat.ma
 Timestamp:
 Apr 3, 2013, 5:54:34 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extranat.ma
r2824 r3081 13 13 ] 14 14 ]. 15 16 lemma 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. 15 27 16 28 inductive nat_compared : nat → nat → Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.