proposition: Theorem even_plus_four : forall n:nat, even n -> even (4+n).
proof: Proof. intros n H. elim H using Even_induction with (P0 := fun n => odd (4+n)); simpl;repeat constructor;assumption. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List