~/jendhub

def internal_div_le_add_cancel

bend-mathlib@0.8.1.0 · nat.bend:895

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

895def internal_div_le_add_cancel(t: Nat, +x: Nat, +y: Nat) -> {Nat.is_le(x, y) == Nat.is_le(Nat.add(t, x), Nat.add(t, y)) : Bool}:
896  match t:
897    case 0n:
898      {==}
899    case 1n+tp:
900      internal_div_le_add_cancel(tp, x, y)

Uses (4)

Used by (1)