law sorted_le_of_mem

bend-mathlib@0.8.1.0 · list.bend:1032

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

1032# The head of a Nat list sorted by Nat.is_le is <= every member of the list.
1033law sorted_le_of_mem:
1034  for x: Nat
1035  for xs: List<&2, Nat>
1036  for y: Nat
1037  for hs: sorted_by(~Nat, ~Nat.is_le, x <> xs)
1038  for hm: mem(~Nat, ~Nat.is_eq, y, x <> xs)
1039  MNat.le(x, y)