proposition: Lemma lor_ones_low : forall a n, log2 a < n -> lor a (ones n) == ones n.
proof: Proof. intros a n 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. - now rewrite ones_spec_low, orb_true_r. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog