~/jendhub

law sorted_head_le_mem

bend-mathlib@0.8.1.0 · list.bend:1012

import bend-mathlib@0.8.1.0/list.bend as List
import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

1012# The head of a Nat list sorted by Nat.is_le is <= every member of its tail.
1013law sorted_head_le_mem:
1014  for x: Nat
1015  for xs: List<&2, Nat>
1016  for y: Nat
1017  for hs: sorted_by(~Nat, ~Nat.is_le, x <> xs)
1018  for hm: mem(~Nat, ~Nat.is_eq, y, xs)
1019  MNat.le(x, y)

Uses (8)

Used by (1)