proposition: Lemma log2_land : forall a b, log2 (land a b) <= min (log2 a) (log2 b).
proof: Proof. assert (AUX : forall a b, a<=b -> log2 (land a b) <= log2 a). { intros a b H. apply le_ngt. intros H'. destruct (eq_decidable (land a b) 0) as [EQ|NEQ]. - rewrite EQ in H'. apply log2_lt_cancel in H'. generalize (le_0_l a); order. - generalize (bit_log2 (land a b) NEQ). now rewrite land_spec, bits_above_log2. } intros a b. destruct (le_ge_cases a b) as [H|H]. - rewrite min_l by now apply log2_le_mono. now apply AUX. - rewrite min_r by now apply log2_le_mono. rewrite land_comm. now apply AUX. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog