proposition: Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b.
proof: Proof. elim (Even_or_Odd a); [intros (a',H)| intros (a',H)]. - exists a'. exists false. now nzsimpl. - exists a'. exists true. now simpl. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog