[Agda] Bezonas helpon !

[Serge Leblanc]

Dear All,
I need help to finish these lemmas.
They have the same meaning, I am right?
All helpers are welcome!

Estimata ĉiuj,
Mi bezonas helpon por daŭrigi ci-tiuj pruvojn!
Ĉu ili havas je la saman signifon! Ĉu mi pravas?
Ĉiuj helpantoj estas bonvenaj!

Sincere.
-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170806/5488f491/attachment.html>
-------------- next part --------------
module Maximal where

open import Data.Nat public using (ℕ; zero; suc; _⊔_; _≤_; _≥_)
open import Data.List.NonEmpty using (List⁺; foldr₁; _∷_;  _∷⁺_; [_]; toList)
open import Data.List.Any as Any using (Any; here; there)
open import Data.List.All as All -- using (All)

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)

max : List⁺ ℕ → ℕ
max l = foldr₁ _⊔_ l

private
  max² : max [ 2 ] ≡ 2
  max² = refl

  max⁵ : max (4 ∷⁺ 5 ∷⁺ [ 6 ]) ≡ 6
  max⁵ = refl



proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max xs)) (toList xs)
proof₁ (s ∷ l) =  {!  !}

open Any.Membership-≡ using (_∈_)

proof₂ : (xs : List⁺ ℕ) → (∀ {x} → x ∈ (toList xs) → (_≥_ (max xs)) x)
proof₂ (s ∷ l) = {!  !}
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170806/5488f491/attachment.sig>