### Nuprl Lemma : div-cancel

`∀[x:ℤ]. ∀[y:ℤ-o].  ((x * y) ÷ y ~ x)`

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` uall: `∀[x:A]. B[x]` divide: `n ÷ m` multiply: `n * m` int: `ℤ` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` top: `Top` sq_type: `SQType(T)` all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}`
Lemmas referenced :  subtype_base_sq int_subtype_base mul-commutes divide-exact int_nzero_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination because_Cache independent_isectElimination hypothesis sqequalRule hypothesisEquality isect_memberEquality voidElimination voidEquality dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination sqequalAxiom intEquality

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[y:\mBbbZ{}\msupminus{}\msupzero{}].    ((x  *  y)  \mdiv{}  y  \msim{}  x)

Date html generated: 2016_05_14-AM-07_24_10
Last ObjectModification: 2015_12_26-PM-01_29_41

Theory : int_2

Home Index