~/jendhub

def le_double

stelliferous@0.0.2.0 · proofs/nat_order.bend:192

import stelliferous@0.0.2.0/proofs/nat_order.bend as NatOrder
import Base
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition

192def le_double(+a: Nat) -> {Nat.is_le(a,Nat.double(a)) == True{} : Bool}:
193  %Addition.double(a) : {Nat.is_le(a,_) == True{} : Bool}
194  le_add(a,a)

Uses (6)

Used by (1)