---

Step * of Lemma rpolydiv-rec

∀[n:ℤ]. ∀[a,z:Top].
  ((rpolydiv(n;a;z) (n - 1) ~ a n) ∧ (∀i:ℕn - 1. (rpolydiv(n;a;z) i ~ (a (i + 1)) + (z * (rpolydiv(n;a;z) (i + 1))))))
BY
{ (Intros THEN D 0) }

1
1. [n] : ℤ
2. [a] : Top
3. [z] : Top
⊢ rpolydiv(n;a;z) (n - 1) ~ a n

2
1. [n] : ℤ
2. [a] : Top
3. [z] : Top
⊢ ∀i:ℕn - 1. (rpolydiv(n;a;z) i ~ (a (i + 1)) + (z * (rpolydiv(n;a;z) (i + 1))))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[a,z:Top].
    ((rpolydiv(n;a;z)  (n  -  1)  \msim{}  a  n)
    \mwedge{}  (\mforall{}i:\mBbbN{}n  -  1.  (rpolydiv(n;a;z)  i  \msim{}  (a  (i  +  1))  +  (z  *  (rpolydiv(n;a;z)  (i  +  1))))))


By

---

Latex:
(Intros  THEN  D  0)

---

Home Index