---

Step * of Lemma decidable__divides_ext

∀a,b:ℤ.  Dec(a | b)
BY
{ Extract of Obid: decidable__divides
  not unfolding  remainder
  finishing with Auto
  normalizes to:
  
  λa,b. if a=0
        then if b=0 then inl <0, Ax> else (inr (λ%4.Ax) )
        else if b rem a=0 then inl <fst(divrem(b; a)), Ax> else (inr (λ%.Ax) ) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    Dec(a  |  b)


By

---

Latex:
Extract  of  Obid:  decidable\_\_divides
not  unfolding    remainder
finishing  with  Auto
normalizes  to:

\mlambda{}a,b.  if  a=0
            then  if  b=0  then  inl  ɘ,  Ax>  else  (inr  (\mlambda{}\%4.Ax)  )
            else  if  b  rem  a=0  then  inl  <fst(divrem(b;  a)),  Ax>  else  (inr  (\mlambda{}\%.Ax)  )

---

Home Index