This commit is contained in:
Thomas Baruchel 2022-12-10 23:08:37 +01:00
parent 6c015eff1d
commit 5f373c7859

View File

@ -1225,7 +1225,7 @@ Proof.
rewrite H1. easy. easy.
rewrite Nat.le_succ_l in H1. apply Nat.pow_lt_mono_r with (a := 2) in H1.
rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption.
apply Nat.lt_1_2. rewrite tm_step_head_1. simpl. reflexivity.
apply Nat.lt_1_2. rewrite tm_step_head_1. reflexivity.
(* k < 0 *)
rename H0 into G.