---

Step * of Lemma omral_times_non_zero_vals

∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.  ((¬↑(0 ∈b map(λx.(snd(x));qs))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));ps ** qs))))
BY
{ (InductionOnList
   THEN (InstLemma `cdrng_is_abdmonoid` [⌜r⌝]⋅ THENA Auto)
   THEN Reduce 0
   THEN Intros
   THEN DProds
   THEN Reduce 0
   THEN Try (Backchain ``    omral_scale_non_zero_vals    omral_plus_non_zero_vals``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps,qs:(|g|  \mtimes{}  |r|)  List.
    ((\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));qs)))  {}\mRightarrow{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps  **  qs))))


By

---

Latex:
(InductionOnList
  THEN  (InstLemma  `cdrng\_is\_abdmonoid`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Intros
  THEN  DProds
  THEN  Reduce  0
  THEN  Try  (Backchain  ``        omral\_scale\_non\_zero\_vals        omral\_plus\_non\_zero\_vals``)
  THEN  Auto)

---

Home Index