proposition: Lemma lor_ones_low : forall a n, 0<=a -> log2 a < n -> lor a (ones n) == 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; try split; trivial. + now apply lt_le_trans with n. + apply le_trans with (log2 a); order_pos. - rewrite ones_spec_low, orb_true_r; try split; trivial. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog