proposition: Lemma add_b2n_double_bit0 : forall (a0:bool) a, (a0+2*a).[0] = a0.
proof: Proof. intros a0 a. apply b2n_inj. rewrite testbit_spec'. nzsimpl. rewrite mul_comm, mod_add by order'. now rewrite mod_small by (destruct a0; order'). Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog