proposition: Lemma log2_lxor : forall a b, 0<=a -> 0<=b -> log2 (lxor a b) <= max (log2 a) (log2 b).
proof: Proof. assert (AUX : forall a b, 0<=a -> a<=b -> log2 (lxor a b) <= log2 b). { intros a b Ha Hb. apply le_ngt. intros LT. assert (H : 0 <= lxor a b) by (apply lxor_nonneg; split; order). le_elim H. - generalize (bit_log2 (lxor a b) H). rewrite lxor_spec, 2 bits_above_log2; try order. + discriminate. + apply le_lt_trans with (log2 b); trivial. now apply log2_le_mono. - 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 max_r by now apply log2_le_mono. now apply AUX. - rewrite max_l by now apply log2_le_mono. rewrite lxor_comm. now apply AUX. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog