proposition: Lemma lxor_spec a b n : testbit (lxor a b) n = xorb (testbit a n) (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, ?xorb_false_l, ?xorb_false_r; trivial; unfold lxor; rewrite ?testbit_Zpos, ?testbit_Zneg, ?testbit_of_N', ?N.pos_pred_succ by trivial. - now rewrite <- N.lxor_spec. - now rewrite N.lxor_spec, negb_xorb_r. - now rewrite N.lxor_spec, negb_xorb_l. - now rewrite N.lxor_spec, xorb_negb_negb. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass