example of search

search.agda

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat hiding (_+_; _<_)

open import Data.Nat
open import Data.Nat.Properties

open import Relation.Binary


-- C-c C-z RET _*_ _≡_ RET
-- returns

-- Definitions about _*_, _≡_
--   *-cancelʳ-≡
--             : (m n : ℕ) {o : ℕ} → m * suc o ≡ n * suc o → m ≡ n
--   *-cancelˡ-≡
--             : {m n : ℕ} (o : ℕ) → m + o * m ≡ n + o * n → m ≡ n
--   *-suc     : (m n : ℕ) → m * suc n ≡ m + m * n
--   +-*-suc   : (m n : ℕ) → m * suc n ≡ m + m * n
--   ^-*-assoc : (m n o : ℕ) → ((m ^ n) ^ o) ≡ (m ^ (n * o))
--   ^-distribˡ-+-*
--             : (m n o : ℕ) → (m ^ (n + o)) ≡ (m ^ n) * (m ^ o)
--   cancel-*-right
--             : (m n : ℕ) {o : ℕ} → m * suc o ≡ n * suc o → m ≡ n
--   i*j≡0⇒i≡0∨j≡0
--             : (m : ℕ) {n : ℕ} → m * n ≡ 0 → m ≡ 0 Data.Sum.Base.⊎ n ≡ 0
--   i*j≡1⇒i≡1 : (m n : ℕ) → m * n ≡ 1 → m ≡ 1
--   i*j≡1⇒j≡1 : (m n : ℕ) → m * n ≡ 1 → n ≡ 1
--   im≡jm+n⇒[i∸j]m≡n
--             : (i j m n : ℕ) → i * m ≡ j * m + n → (i ∸ j) * m ≡ n
--   m*n≡0⇒m≡0∨n≡0
--             : (m : ℕ) {n : ℕ} → m * n ≡ 0 → m ≡ 0 Data.Sum.Base.⊎ n ≡ 0
--   m*n≡1⇒m≡1 : (m n : ℕ) → m * n ≡ 1 → m ≡ 1
--   m*n≡1⇒n≡1 : (m n : ℕ) → m * n ≡ 1 → n ≡ 1