proposition: Lemma log2_lor : forall a b, 0<=a -> 0<=b -> log2 (lor a b) == max (log2 a) (log2 b).
proof: Proof. assert (AUX : forall a b, 0<=a -> a<=b -> log2 (lor a b) == log2 b). { intros a b Ha H. le_elim Ha; [|now rewrite <- Ha, lor_0_l]. apply log2_bits_unique. - now rewrite lor_spec, bit_log2, orb_true_r by order. - intros m Hm. assert (H' := log2_le_mono _ _ H). now rewrite lor_spec, 2 bits_above_log2 by order. } intros a b Ha Hb. destruct (le_ge_cases a b) as [H|H]. - rewrite max_r by now apply log2_le_mono. now apply AUX. - rewrite max_l by now apply log2_le_mono. rewrite lor_comm. now apply AUX. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog