---

Step * 1 of Lemma rational_set_blt


1. a2 : ℤ
2. a1 : ℤ
⊢ (0 <z a1 + ((-1) * a2) ∨b(a2 =z a1)) ∧b (¬b(0 <z a2 + ((-1) * a1) ∨b(a1 =z a2))) = a2 <z a1
BY
{ TACTIC:((RW IntNormC 0⋅ THENA Auto)
          THEN Try (AutoSplit)
          THEN (RWW "band_ff_simp band_tt_simp bor_ff_simp" 0 THENA Auto)
          THEN Reduce 0
          THEN (BLemma `iff_imp_equal_bool` THENM RW assert_pushdownC 0)
          THEN Auto) }

---

Latex:

---

Latex:

1.  a2  :  \mBbbZ{}
2.  a1  :  \mBbbZ{}
\mvdash{}  (0  <z  a1  +  ((-1)  *  a2)  \mvee{}\msubb{}(a2  =\msubz{}  a1))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(0  <z  a2  +  ((-1)  *  a1)  \mvee{}\msubb{}(a1  =\msubz{}  a2)))  =  a2  <z  a1


By

---

Latex:
TACTIC:((RW  IntNormC  0\mcdot{}  THENA  Auto)
                THEN  Try  (AutoSplit)
                THEN  (RWW  "band\_ff\_simp  band\_tt\_simp  bor\_ff\_simp"  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (BLemma  `iff\_imp\_equal\_bool`  THENM  RW  assert\_pushdownC  0)
                THEN  Auto)

---

Home Index