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

[Andreas Abel]

On 31.10.14 8:05 PM, Nils Anders Danielsson wrote:
> 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.

Which is a direct consequence of the positive statement

   _∪-Finite_ : ∀ {P Q} → Finite P → Finite Q → Finite (P ∪ Q)

modulo some de Morgan and contraposition obfuscation.