def internal_le_of_mem_step

bend-mathlib@0.8.1.0 · list.bend:1024

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

1024def internal_le_of_mem_step(+x: Nat, xs: List<&2, Nat>, +y: Nat, b: Bool, e: {Nat.is_eq(x, y) == b : Bool}, hs: sorted_by(~Nat, ~Nat.is_le, x <> xs), hm: {Bool.or(b, List.contains(~Nat, ~Nat.is_eq, xs, y)) == True{} : Bool}) -> MNat.le(x, y):
1025  match b:
1026    case True{}:
1027      %MNat.eq_of_is_eq(x, y, e) : MNat.le(x, _)
1028      MNat.le_refl(x)
1029    case False{}:
1030      sorted_head_le_mem(x, xs, y, hs, hm)