proposition: Lemma ev_Even_firsttry : forall n, ev n -> Even n.
proof: Proof. unfold Even. intros n E. inversion E as [EQ' | n' E' EQ']. - exists 0. reflexivity. - assert (H: (exists k', n' = double k') -> (exists n0, S (S n') = double n0)). { intros [k' EQ'']. exists (S k'). simpl. rewrite <- EQ''. reflexivity. } apply H. generalize dependent E'. Abort. 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)