proposition: Lemma domain_P1 : forall X:R -> Prop, ~ (exists y : R, X y) \/ (exists y : R, X y /\ (forall x:R, X x -> x = y)) \/ (exists x : R, (exists y : R, X x /\ X y /\ x <> y)).
proof: Proof. intro; elim (classic (exists y : R, X y)); intro. - right; elim H; intros; elim (classic (exists y : R, X y /\ y <> x)); intro. + right; elim H1; intros; elim H2; intros; exists x; exists x0; intros. split; [ assumption | split; [ assumption | apply (not_eq_sym (A:=R)); assumption ] ]. + left; exists x; split. * assumption. * intros; case (Req_dec x0 x); intro. -- assumption. -- elim H1; exists x0; split; assumption. - left; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type