clean up
group related lemmas
generalize "3∣sn⇒quot<sn" to "2+m∣1+n⇒quot<1+n"

3∣sn⇒quot<sn : ∀ {n} → (3∣sn : 3 ∣ suc n) → (quotient 3∣sn < suc n)
2+m∣1+n⇒quot<1+n : ∀ {m} {n} → (2+m∣1+n : 2 + m ∣ 1 + n) → (quotient 2+m∣1+n < 1 + n)