proposition: Theorem ev_double : forall n, ev (double n).
proof: Proof. Admitted. Theorem ev_inversion : forall (n : nat), ev n -> (n = 0) \/ (exists n', n = S (S n') /\ ev n'). Proof. intros n E. destruct E as [ | n' E'] eqn:EE. - left. reflexivity. - right. exists n'. split. reflexivity. apply E'. Qed.
imports: Coq(Lia)