---

Step * of Lemma pv11_p1_lt_bnum_trans2

∀ldrs_uid:Id ⟶ ℤ. ∀b1,b2,b3:pv11_p1_Ballot_Num().
  ((↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ⇒ (↑(b2  < b3)) ⇒ (↑(b1  < b3)))
BY
{ (Auto THEN SimpleReasoningSteps) }

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b1,b2,b3:pv11\_p1\_Ballot\_Num().
    ((\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b1  b2))  {}\mRightarrow{}  (\muparrow{}(b2    <  b3))  {}\mRightarrow{}  (\muparrow{}(b1    <  b3)))


By

---

Latex:
(Auto  THEN  SimpleReasoningSteps)

---

Home Index