src/HOL/Library/Binomial.thy
changeset 25112 98824cc791c0
parent 21263 de65ce2bfb32
child 25134 3d4953e88449
     1.1 --- a/src/HOL/Library/Binomial.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Library/Binomial.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -50,11 +50,11 @@
     1.4  lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
     1.5    apply (safe intro!: binomial_eq_0)
     1.6    apply (erule contrapos_pp)
     1.7 -  apply (simp add: zero_less_binomial)
     1.8 +  apply (simp add: neq0_conv zero_less_binomial)
     1.9    done
    1.10  
    1.11  lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
    1.12 -  by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
    1.13 +  by (simp add: neq0_conv  linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
    1.14  
    1.15  (*Might be more useful if re-oriented*)
    1.16  lemma Suc_times_binomial_eq: