From dc91289017b86482c00c5178d66e904b2531e5f8 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 10 Dec 2022 14:56:42 +0100 Subject: [PATCH] Update --- thue-morse.v | 24 ------------------------ 1 file changed, 24 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index a54b476..f190a16 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1416,30 +1416,6 @@ Require Import BinPos. -(* -PeanoNat.Nat.log2_spec_alt: - forall a : nat, - 0 < a -> - exists r : nat, - a = 2 ^ PeanoNat.Nat.log2 a + r /\ 0 <= r < 2 ^ PeanoNat.Nat.log2 a -N.log2_spec_alt: - forall a : N, - (0 < a)%N -> - exists r : N, a = (2 ^ N.log2 a + r)%N /\ (0 <= r < 2 ^ N.log2 a)%N - - -PeanoNat.Nat.log2_shiftl: - forall a n : nat, - a <> 0 -> - PeanoNat.Nat.log2 (PeanoNat.Nat.shiftl a n) = PeanoNat.Nat.log2 a + n - - - - *) - - - - (* Hamming weight of a positive; argument can not be 0! *) Fixpoint hamming_weight_positive (x: positive) := match x with