proposition: Lemma ldiff_ones_r : forall a n, 0<=n -> ldiff a (ones n) == (a >> n) << n.
proof: Proof. intros a n Hn. 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 apply le_0_sub. + now split. - rewrite ones_spec_low, shiftl_spec_low, andb_false_r; try split; trivial. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog