proposition: Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
proof: Proof. intros n H. apply ev_inversion in H. destruct H as [H0|H1]. - discriminate H0. - destruct H1 as [n' [Hnm Hev]]. injection Hnm as Heq. rewrite Heq. apply Hev. Qed.
imports: Coq(Lia)