[Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...

[Nils Anders Danielsson]

On 2014-10-25 17:18, Sergei Meshveliani wrote:
> I have been asked about a constructive proof of this theorem:
>
>    ℕ ⊆ P U Q -> (¬ isFinite P) ⊎ (¬ isFinite Q).

Some respondents have noted things that are not provable. The following
statement is provable:

   ¬ isFinite (P ∪ Q) → ¬ ¬ ((¬ isFinite P) ⊎ (¬ isFinite Q))

See Data.Nat.InfinitelyOften in the standard library.

-- 
/NAD