proposition: Lemma log2_1_inv : forall a, Zpos (log2 a) = 1 -> a = xH.
proof: Proof. destruct a;simpl;zsimpl;intros;trivial. assert (H1:= Zlt_0_pos (log2 a));exfalso;lia. assert (H1:= Zlt_0_pos (log2 a));exfalso;lia. Qed.
imports: ZArith Lia ZCmisc