2013-09-19から1日間の記事一覧
(* ev_ev_even *) Theorem ev_ev_even : forall n m, ev (n+ m) -> ev n -> ev m. Proof. intros n m E1 E2. induction E2 as [|n' E']. Case "E2 = ev_O'". simpl in E1. apply E1. Case "E2 = ev_SS n'". simpl in E1. inversion E1 as [|p E1']. apply IH…