proposition: Lemma log2_land : forall a b, 0<=a -> 0<=b -> log2 (land a b) <= min (log2 a) (log2 b).
proof: Proof. assert (AUX : forall a b, 0<=a -> a<=b -> log2 (land a b) <= log2 a). { intros a b Ha Hb. apply le_ngt. intros LT. assert (H : 0 <= land a b) by (apply land_nonneg; now left). le_elim H. - generalize (bit_log2 (land a b) H). now rewrite land_spec, bits_above_log2. - rewrite <- H in LT. apply log2_lt_cancel in LT; order. } intros a b Ha Hb. 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 ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog