proposition: Theorem dist_not_exists : forall (X:Type) (P : X -> Prop), (forall x, P x) -> ~ (exists x, ~ P x).
proof: Proof. Admitted. Theorem dist_exists_or : forall (X:Type) (P Q : X -> Prop), (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x). 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. simpl. right. right. right. left. reflexivity. Qed.