proposition: Lemma ldiff_spec a b n : testbit (ldiff a b) n = testbit a n && negb (testbit b n).
proof: Proof. destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r]. destruct a as [ |a|a], b as [ |b|b]; rewrite ?testbit_0_l, ?andb_true_r; trivial; unfold ldiff; rewrite ?testbit_Zpos, ?testbit_Zneg, ?testbit_of_N', ?N.pos_pred_succ by trivial. - now rewrite <- N.ldiff_spec. - now rewrite N.land_spec, negb_involutive. - now rewrite N.lor_spec, negb_orb. - now rewrite N.ldiff_spec, negb_involutive, andb_comm. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass