proposition: Theorem log2_div2 : forall x y, S y = Nat.log2 x -> Nat.log2 (Nat.div2 x) = y.
proof: Proof. intuition. specialize (Nat.log2_double); intuition. destruct (@nat_half_plus x). eapply Nat.log2_lt_cancel. rewrite Nat.log2_1. lia. destruct H1. intuition. subst. destruct x1. rewrite Nat.add_0_r in *. rewrite Nat.div2_double. rewrite H0 in H. lia. lia. destruct x1. rewrite Nat.add_comm. rewrite Nat.add_1_l, Nat.div2_succ_double. rewrite Nat.log2_succ_double in H. lia. lia. lia. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat