proposition: Lemma log2_lxor : forall a b, log2 (lxor a b) <= max (log2 a) (log2 b).
proof: Proof. assert (AUX : forall a b, a<=b -> log2 (lxor a b) <= log2 b). { intros a b H. apply le_ngt. intros H'. destruct (eq_decidable (lxor 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 (lxor a b) NEQ). rewrite lxor_spec, 2 bits_above_log2; try order. + discriminate. + apply le_lt_trans with (log2 b); trivial. now apply log2_le_mono. } intros a b. 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 NAxioms NSub NPow NDiv NParity NLog