proposition: Theorem ev_sum : forall n m, ev n -> ev m -> ev (n + m).
proof: Proof. Admitted. Inductive ev' : nat -> Prop := | ev'_0 : ev' 0 | ev'_2 : ev' 2 | ev'_sum n m (Hn : ev' n) (Hm : ev' m) : ev' (n + m). Theorem ev'_ev : forall n, ev' n <-> ev n. Proof. Admitted. Theorem ev_ev__ev : forall n m, ev (n+m) -> ev n -> ev m. Proof. Admitted. Theorem ev_plus_plus : forall n m p, ev (n+m) -> ev (n+p) -> ev (m+p). Proof. Admitted. Module Playground. Inductive le : nat -> nat -> Prop := | le_n (n : nat) : le n n | le_S (n m : nat) (H : le n m) : le n (S m). Notation "n <= m" := (le n m). Theorem test_le1 : 3 <= 3. Proof. apply le_n. Qed.
imports: Coq(Lia)