def internal_div_le_self_eq
bend-mathlib@0.8.1.0 · nat.bend:1968
import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base
1968def internal_div_le_self_eq(+q: Nat, +bp: Nat, +m: Nat, -a: Nat, e: {Nat.add(Nat.mul(q, 1n+bp), m) == a : Nat}) -> {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == a : Nat}:
1969 %e : {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == _ : Nat}
1970 %mul_comm(1n+bp, q) : {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == Nat.add(_, m) : Nat}
1971 Equal.sym(Nat, Nat.add(Nat.add(q, Nat.mul(bp, q)), m), Nat.add(q, Nat.add(Nat.mul(bp, q), m)), add_assoc(q, Nat.mul(bp, q), m))