proposition: Lemma ev_Even_firsttry : forall n, ev n -> Even n.
proof: Proof. Admitted. Lemma ev_Even : forall n, ev n -> Even n. Proof. intros n E. induction E as [|n' E' IH]. - unfold Even. exists 0. reflexivity. - unfold Even in IH. destruct IH as [k Hk]. rewrite Hk. unfold Even. exists (S k). simpl. reflexivity. Qed.
imports: Coq(Lia)