proposition: Lemma add_b2z_double_div2 : forall (a0:bool) a, (a0+2*a)/2 == a.
proof: Proof. intros a0 a. rewrite mul_comm, div_add by order'. now rewrite div_small, add_0_l by (destruct a0; split; simpl; order'). Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog