proposition: Lemma ldiff_ones_l_low : forall a n, 0<=a -> log2 a < n -> ldiff (ones n) a == lxor a (ones n).
proof: Proof. intros a n Ha H. bitwise as m ?. destruct (le_gt_cases n m). - rewrite ones_spec_high, bits_above_log2; trivial. + now apply lt_le_trans with n. + split; trivial. now apply le_trans with (log2 a); order_pos. - rewrite ones_spec_low, xorb_true_r; try split; trivial. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog