From 4e3641242ddea22c7ac1b171440497d27c8352bf Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 29 Dec 2022 11:00:10 +0100 Subject: [PATCH] Update --- thue-morse.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index ca32d13..9c3ac0f 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -735,11 +735,10 @@ Proof. rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r. rewrite <- Nat.sub_succ_l. rewrite Nat.sub_succ. reflexivity. - replace (2) with (2*1) at 1. + rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_pos_l. apply Nat.lt_0_2. apply Nat.le_succ_l. apply Nat.mul_pos_pos. - apply Nat.lt_0_succ. assumption. apply Nat.mul_1_r. - apply Nat.lt_0_2. + apply Nat.lt_0_succ. assumption. apply Nat.lt_0_2. apply Nat.mul_comm. apply Nat.mul_comm. Qed.