Update
This commit is contained in:
parent
de7cc14376
commit
dd2bd9d4f5
@ -1190,6 +1190,9 @@ Proof.
|
||||
generalize H2. generalize J. apply Nat.le_trans.
|
||||
Qed.
|
||||
|
||||
(* Note: a first version included the 0 < k hypothesis but in the very
|
||||
unorthodox case where k=0 it happens to be true anyway, and the hypothesis
|
||||
was removed in order to make the theorem more general *)
|
||||
Theorem tm_step_flip_low_bit :
|
||||
forall (n m k j : nat),
|
||||
j < m -> k * 2^m < 2^n
|
||||
@ -1212,8 +1215,7 @@ Proof.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
apply Nat.le_0_l. assumption.
|
||||
|
||||
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases.
|
||||
destruct G.
|
||||
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G.
|
||||
|
||||
(* k = 0 *)
|
||||
rewrite H0. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
|
||||
|
Loading…
Reference in New Issue
Block a user