proposition: Lemma odd_bitwise : forall op n a b, odd (bitwise op (S n) a b) = op (odd a) (odd b).
proof: Proof. intros op n a b; unfold bitwise; fold bitwise. destruct (op (odd a) (odd b)). - apply odd_spec. rewrite add_comm; eexists; eauto. - unfold odd; apply negb_false_iff. apply even_spec. rewrite add_0_l; eexists; eauto. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass