---

Step * of Lemma combinations-positive

∀[n:ℕ]. ∀[m:ℤ].  0 < C(n;m) supposing n ≤ m
BY
{ xxx((InductionOnNat THEN Auto)
      THEN (RWO "combinations-step" 0 THENA Auto)
      THEN Reduce 0
      THEN Auto
      THEN OldAutoSplit)xxx }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbZ{}].    0  <  C(n;m)  supposing  n  \mleq{}  m


By

---

Latex:
xxx((InductionOnNat  THEN  Auto)
        THEN  (RWO  "combinations-step"  0  THENA  Auto)
        THEN  Reduce  0
        THEN  Auto
        THEN  OldAutoSplit)xxx

---

Home Index