proposition: Lemma In_map_iff : forall (A B : Type) (f : A -> B) (l : list A) (y : B), In y (map f l) <-> exists x, f x = y /\ In x l.
proof: Proof. Admitted. Lemma in_app_iff : forall A l l' (a:A), In a (l++l') <-> In a l \/ In a l'. Proof. Admitted. Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop . Admitted. Lemma All_In : forall T (P : T -> Prop) (l : list T), (forall x, In x l -> P x) <-> All P l. Proof. Admitted. Definition combine_odd_even (Podd Peven : nat -> Prop) : nat -> Prop . Admitted. Theorem combine_odd_even_intro : forall (Podd Peven : nat -> Prop) (n : nat), (oddb n = true -> Podd n) -> (oddb n = false -> Peven n) -> combine_odd_even Podd Peven n. Proof. Admitted. Theorem combine_odd_even_elim_odd : forall (Podd Peven : nat -> Prop) (n : nat), combine_odd_even Podd Peven n -> oddb n = true -> Podd n. Proof. Admitted. Theorem combine_odd_even_elim_even : forall (Podd Peven : nat -> Prop) (n : nat), combine_odd_even Podd Peven n -> oddb n = false -> Peven n. Proof. Admitted. Check plus_comm. Lemma plus_comm3 : forall n m p, n + (m + p) = (p + m) + n. Proof. intros n m p. rewrite plus_comm. rewrite plus_comm. Abort. Lemma plus_comm3_take2 : forall n m p, n + (m + p) = (p + m) + n. Proof. intros n m p. rewrite plus_comm. assert (H : m + p = p + m). { rewrite plus_comm. reflexivity. } rewrite H. reflexivity. Qed.
imports: Tactics