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