proposition: Theorem OddSEvenInv : forall n : Z, Odd (Z.succ n) -> Even n.
proof: Proof. intros n H'; case H'; intros m H'1; exists m. apply Z.succ_inj; rewrite H'1; (unfold Z.succ in |- *; ring). Qed.
imports: Reals ZArith List PeanoNat Psatz