def qone
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/final.bend:302
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/final.bend as Final
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as ST
302def qone(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +hc: {Nat.is_eq(qq(h), 0n) == False{} : Bool}) -> {qq(h) == 1n : Nat}:
303 N.le_antisym(qq(h), 1n, N.lt_succ_le(qq(h), 1n, qlt2(one, h1, h, hh)), N.lt_succ_le_succ(0n, qq(h), N.lt_or_eq(0n, qq(h), N.zero_le(qq(h)), N.is_eq_sym_false(qq(h), 0n, hc))))