Theorem eq-dist

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: abs-ls-same-01, dist-lsplit, dist-rmerge, dist-sub-merge, dist-sub-split, numdist, numeq-01, numsub, numsucc, pred-rmerge, succ-rmerge, two-pred, two-sub, zero-gr-add-02,
• Used by units in proved state: int-pot, int-gcd, int-div, intnat, int-square, int-min,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 1
• Used lemmas: commutativity, associativity, dist-rsplit,
• Used spec theorems:
  • Used simplifier rules:
    • int-basic2/add-in
    • int-basic2/add-c
    • int-basic2/add-a