proposition: Lemma log2_bits_unique : forall a n, a.[n] = true -> (forall m, n<m -> a.[m] = false) -> log2 a == n.
proof: Proof. intros a n H H'. destruct (lt_trichotomy a 0) as [Ha|[Ha|Ha]]. - destruct (proj1 (bits_iff_neg_ex a) Ha) as (k,Hk). destruct (le_gt_cases n k). + specialize (Hk (S k) (lt_succ_diag_r _)). rewrite H' in Hk. * discriminate. * apply lt_succ_r; order. + specialize (H' (S n) (lt_succ_diag_r _)). rewrite Hk in H'. * discriminate. * apply lt_succ_r; order. - now rewrite Ha, bits_0 in H. - apply le_antisymm; apply le_ngt; intros LT. + specialize (H' _ LT). now rewrite bit_log2 in H'. + now rewrite bits_above_log2 in H by order. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog