proposition: Lemma ldiff_ones_r : forall a n, ldiff a (ones n) == (a >> n) << n.
proof: Proof. intros a n. bitwise as m. destruct (le_gt_cases n m). - rewrite ones_spec_high, shiftl_spec_high', shiftr_spec'; trivial. rewrite sub_add; trivial. apply andb_true_r. - now rewrite ones_spec_low, shiftl_spec_low, andb_false_r. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog