proposition: Lemma lor_spec a b n : testbit (lor a b) n = 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, ?orb_false_r; trivial; unfold lor; rewrite ?testbit_Zpos, ?testbit_Zneg, ?N.pos_pred_succ by trivial. - now rewrite <- N.lor_spec. - now rewrite N.ldiff_spec, negb_andb, negb_involutive, orb_comm. - now rewrite N.ldiff_spec, negb_andb, negb_involutive. - now rewrite N.land_spec, negb_andb. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass