- Data.Nat.Properties has
m∸n≤m⊔n : ∀ m n → m ∸ n ≤ m ⊔ n
Probably it is not needed because it is proved only by
≤-trans (m∸n≤m m n) (m≤m⊔n m n)
- Algebra.Definitions has
Identical : Op₂ A → Set _
Identical _∙_ = ∀ x y z → ((z ∙ x) ∙ (y ∙ z)) ≈ (z ∙ ((x ∙ y) ∙ z))
The name is not meaningful. Generally, many pairs of expressions are identical in algebra.
- Disagreement between (LeftInvertible ≈ ε ∙ x) and (x ∣ ε) in Monoid.
For example,
lemma : ∀ x → LeftInvertible _≈_ ε _∙_ x → x ∣ʳ ε
lemma x invertible-x = invertible-x
is not type-checked.
This is one more argument for returning to the definition of
(x ∣ʳ y) as ∃[ q ] (q ∙ x ≈ y).
Probably it is not needed because it is proved only by
≤-trans (m∸n≤m m n) (m≤m⊔n m n)The name is not meaningful. Generally, many pairs of expressions are identical in algebra.
For example,
is not type-checked.
This is one more argument for returning to the definition of
(x ∣ʳ y)as∃[ q ] (q ∙ x ≈ y).