------------------------------------------------------------------------
-- Properties of _×′_
1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x
1+×′ 0 x = sym (+-identityʳ x)
1+×′ (suc n) x = refl
-- _×_ and _×′_ are extensionally equal (up to the setoid
-- equivalence).
×≈×′ : ∀ n x → n × x ≈ n ×′ x
×≈×′ 0 x = refl
×≈×′ (suc n) x = begin
x + n × x ≈⟨ +-congˡ (×≈×′ n x) ⟩
x + n ×′ x ≈⟨ sym (1+×′ n x) ⟩
suc n ×′ x ∎
which seem to have been omitted in the move over to Algebra.Properties.Monoid.Mult...? Or have I missed something somewhere?
Specifically L72-L87
which seem to have been omitted in the move over to
Algebra.Properties.Monoid.Mult...? Or have I missed something somewhere?NB. Commutativity is a red herring here!