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 (eq_0_gt_0_cases a) as [Ha|Ha]. - now rewrite Ha, bits_0 in H. - apply le_antisymm; apply le_ngt; intros LT. + specialize (H' _ LT). now rewrite bit_log2 in H' by order. + now rewrite bits_above_log2 in H by order. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog