proposition: Lemma lor_spec a b n : testbit (lor a b) n = testbit a n || testbit b n.
proof: Proof. unfold lor; apply testbit_bitwise_2. - trivial. - destruct (compare_spec a b) as [H|H|H]. + rewrite max_l; subst; trivial. + now apply lt_le_incl in H; rewrite max_r. + now apply lt_le_incl in H; rewrite max_l. - destruct (compare_spec a b) as [H|H|H]. + rewrite max_r; subst; trivial. + now apply lt_le_incl in H; rewrite max_r. + now apply lt_le_incl in H; rewrite max_l. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass