proposition: Lemma div2_bitwise : forall op n a b, div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).
proof: Proof. intros op n a b; unfold bitwise; fold bitwise. destruct (op (odd a) (odd b)). - now rewrite div2_succ_double. - now rewrite add_0_l, div2_double. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass