~/bend-docscommunity

proofs/math/typed/natlight.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as Natlight

6 imports
import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./natfuel.bend as NF

Definitions

def dmq source · line 12 · raw

@+x:Nat -> @+D:Nat -> @+hD:{Nat.is_lt(0n, D) == True{} : Bool} -> {Nat.add(Nat.mul(Nat.div(x, D), D), Nat.mod(x, D)) == x : Nat}

def dml source · line 19 · raw

@+x:Nat -> @+D:Nat -> @+hD:{Nat.is_lt(0n, D) == True{} : Bool} -> {Nat.is_lt(Nat.mod(x, D), D) == True{} : Bool}

def mle2 source · line 26 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+hcd:{Nat.is_le(c, d) == True{} : Bool} -> {Nat.is_le(Nat.mul(a, c), Nat.mul(b, d)) == True{} : Bool}

def mul1 source · line 31 · raw

@+y:Nat -> {Nat.mul(1n, y) == y : Nat}

def two_mul source · line 34 · raw

@+S:Nat -> {Nat.mul(S, 2n) == Nat.add(S, S) : Nat}