~/jendhub

def internal_div_wit_succ

bend-mathlib@0.8.1.0 · nat.bend:786

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

786def internal_div_wit_succ(+ap: Nat, +bq: Nat, w: &k:Nat -> {Nat.add(ap, k) == bq : Nat}) -> &k:Nat -> {Nat.add(1n+ap, k) == 1n+bq : Nat}:
787  match w:
788    case (k, e):
789      (k, Equal.cong(Nat, Nat, x => 1n+x, Nat.add(ap, k), bq, e))

Uses (5)

Used by (1)