Changeset 1515 for src/utilities/extranat.ma
- Timestamp:
- Nov 18, 2011, 1:03:14 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/extranat.ma
r961 r1515 1 include "basics/types.ma". 1 2 include "arithmetics/nat.ma". 2 3 … … 36 37 [ // 37 38 | #m' #IH whd in ⊢ (??%?) > IH @refl 39 ] qed. 40 41 42 let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝ 43 match n return λn.Sum (n=m) (n≠m) with 44 [ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ] 45 | S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒ 46 match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ] 47 ]. 48 [ 1,2: % #E destruct 49 | >E @refl 50 | % #E destruct cases NE /2/ 38 51 ] qed. 39 52
Note: See TracChangeset
for help on using the changeset viewer.