def comb

bend-kit-collections@0.1.4.1 · nat_order.bend:105

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

105def comb(+p: Lin, +q: Lin, +r: Lin, +s: Lin, +v: Vs, e1: LE(F(p, v), F(q, v)), e2: LE(F(r, v), F(s, v)))
106  -> LE(F(ladd(p, r), v), F(ladd(q, s), v)):
107  %F_add(p, r, v) : LE(_, F(ladd(q, s), v))
108  %F_add(q, s, v) : LE(Nat.add(F(p, v), F(r, v)), _)
109  MNat.add_le_add(F(p, v), F(r, v), F(q, v), F(s, v), e1, e2)