instance Nat.instDvdNat_1 : Dvd Nat

Divisibility of natural numbers. a ∣ b (typed as \|) says that there is some c such that b = a * c.

Equations

• Nat.instDvdNat_1 = { dvd := fun (a b : Nat) => ∃ (c : Nat), b = a * c }