non-zero.agda

module non-zero where

import Data.Vec as V
open V using (Vec; zip; toList)
open V renaming ([] to v[]; _∷_ to _v∷_)
import Data.List as L
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
open L using (List; []; _∷_; filter)
-- open import Data.List.Relation.Binary.Suffix.Heterogeneous
open import Data.Nat -- using (ℕ; zero; suc; _*_; _+_)
open import Data.Nat.Properties -- using (_≟_)
open import Data.Fin hiding (_≟_; _<_)
open import Relation.Nullary -- using (Dec)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Nullary.Negation
open import Function using (_∘_; _∘′_)
open import Data.Product using (uncurry′; _×_; _,_; proj₁; proj₂; Σ; ∃; Σ-syntax; ∃-syntax)
import Relation.Binary.PropositionalEquality as Eq
open Eq -- using (_≡_; refl; trans; cong; sym; cong₂)

non-zero : (n : ℕ) → Dec (n ≢ zero)
non-zero n = ¬? (n ≟ zero)

postulate
  ¬¬ℕ : {m n : ℕ} → ¬ ¬ (n ≡ m) → n ≡ m

lemma-2 : (xs : List ℕ)
  → L.sum (filter non-zero xs) ≡ L.sum xs
lemma-2 [] = refl
lemma-2 (x ∷ xs) with non-zero x
lemma-2 (x ∷ xs) | yes p rewrite lemma-2 xs = refl
lemma-2 (x ∷ xs) | no ¬p rewrite ¬¬ℕ ¬p | lemma-2 xs = refl