---

Step * of Lemma int-dot-add-right

∀[cs,as,bs:ℤ List].  cs ⋅ as + bs ~ cs ⋅ as + cs ⋅ bs supposing ||as|| = ||bs|| ∈ ℤ
BY
{ (InductionOnList THEN Reduce 0) }

1
∀[as,bs:ℤ List].  0 ~ 0 supposing ||as|| = ||bs|| ∈ ℤ

2
1. u : ℤ
2. v : ℤ List
3. ∀[as,bs:ℤ List].  v ⋅ as + bs ~ v ⋅ as + v ⋅ bs supposing ||as|| = ||bs|| ∈ ℤ
⊢ ∀[as,bs:ℤ List].  [u / v] ⋅ as + bs ~ [u / v] ⋅ as + [u / v] ⋅ bs supposing ||as|| = ||bs|| ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[cs,as,bs:\mBbbZ{}  List].    cs  \mcdot{}  as  +  bs  \msim{}  cs  \mcdot{}  as  +  cs  \mcdot{}  bs  supposing  ||as||  =  ||bs||


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index