~/jendhub

def internal_lt_mul_two_add

bend-mathlib@0.8.1.0 · nat.bend:3360

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

3360def internal_lt_mul_two_add(a: Nat, x: Nat, hx: lt(0n, x)) -> lt(x, Nat.mul(2n+a, x)):
3361  match x:
3362    case 0n:
3363      Empty.absurd(lt(0n, Nat.mul(2n+a, 0n)), internal_false_ne_true(hx))
3364    case 1n++y:
3365      lt_add_of_pos_right(y, Nat.add(y, Nat.mul(a, 1n+y)))

Uses (7)

Used by (1)