From ddfbaa6c8da49d43f8cfdc9adddcdd8fe2d810d5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Feb 2018 14:32:50 -0800 Subject: [PATCH] fix(library/init/data/nat/basic): missing lemma --- library/init/data/nat/basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 8a6a62aeea..bdfb04674c 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -181,6 +181,9 @@ protected lemma zero_lt_bit0 : ∀ {n : nat}, n ≠ 0 → 0 < bit0 n calc 0 < succ (succ (bit0 n)) : zero_lt_succ _ ... = bit0 (succ n) : (nat.bit0_succ_eq n).symm +protected lemma zero_lt_bit1 (n : nat) : 0 < bit1 n := +zero_lt_succ _ + protected lemma bit0_ne_zero : ∀ {n : ℕ}, n ≠ 0 → bit0 n ≠ 0 | 0 h := absurd rfl h | (n+1) h :=