proposition: Theorem ev_double : forall n, ev (double n).
proof: Proof. Admitted. Theorem ev_minus2 : forall n, ev n -> ev (pred (pred n)). Proof. intros n E. inversion E as [| n' E']. - simpl. apply ev_0. - simpl. apply E'. Qed.
imports: Logic