proposition: Lemma bit0_odd : forall a, a.[0] = odd a.
proof: Proof. intros a. symmetry. destruct (exists_div2 a) as (a' & b & EQ). rewrite EQ, testbit_0_r, add_comm, odd_add_mul_2. destruct b; simpl; apply odd_1 || apply odd_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog