proposition: Theorem exists_example_2 : forall n, (exists m, n = 4 + m) -> (exists o, n = 2 + o).
proof: Proof. Admitted. Theorem leb_plus_exists : forall n m, n <=? m = true -> exists x, m = n+x. Proof. Admitted. Theorem plus_exists_leb : forall n m, (exists x, m = n+x) -> n <=? m = true. Proof. Admitted. Fixpoint In {A : Type} (x : A) (l : list A) : Prop := match l with | [] => False | x' :: l' => x' = x \/ In x l' end. Example In_example_1 : In 4 [1; 2; 3; 4; 5]. Proof. Admitted. Example In_example_2 : forall n, In n [2; 4] -> exists n', n = 2 * n'. Proof. Admitted. Theorem In_map : forall (A B : Type) (f : A -> B) (l : list A) (x : A), In x l -> In (f x) (map f l). Proof. intros A B f l x. induction l as [|x' l' IHl']. - simpl. intros []. - simpl. intros [H | H]. + rewrite H. left. reflexivity. + right. apply IHl'. apply H. Qed.