src/HOL/Library/Extended_Nat.thy
changeset 61631 4f7ef088c4ed
parent 61384 9f5145281888
child 62374 cb27a55d868a
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Wed Nov 11 09:48:24 2015 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Nov 11 10:07:27 2015 +0100
     1.3 @@ -459,6 +459,10 @@
     1.4  lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k"
     1.5    by (cases n) simp_all
     1.6  
     1.7 +lemma iadd_le_enat_iff:
     1.8 +  "x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)"
     1.9 +by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
    1.10 +
    1.11  lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j"
    1.12  apply (induct_tac k)
    1.13   apply (simp (no_asm) only: enat_0)