From 63284a15429c682df529b5e0f394314a4a3452ab Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Fri, 27 Jan 2023 17:39:07 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 9479d76..ead0c5b 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1833,7 +1833,22 @@ Proof. apply Nat.le_refl. -Admitted. + + rewrite <- Nat.div_add. rewrite Nat.mul_comm. + replace (2 * Nat.div2 (length a')) + with (2 * Nat.div2 (length a') + Nat.b2n (Nat.odd (length a'))). + rewrite <- Nat.div2_odd. rewrite <- Nat.div2_div. reflexivity. + rewrite <- Nat.negb_even. rewrite J'. simpl. rewrite Nat.add_0_r. + reflexivity. easy. easy. rewrite Nat.div2_div. reflexivity. + rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity. + apply Nat.le_refl. + rewrite <- Nat.div_add. rewrite Nat.mul_comm. + replace (2 * Nat.div2 (length a)) + with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))). + rewrite <- Nat.div2_odd. rewrite <- Nat.div2_div. reflexivity. + rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. + reflexivity. easy. +Qed.