agda-stdlib

agda-stdlib copied to clipboard

I'd like there to be certain properties of the quotient of a proof of divisibility, for example:

foo : ∀ {m n} → (m∣n : m ∣ n) → quotient m∣n ∣ n
bar : ∀ {m n} (m∣n : m ∣ n) → m > 1 → quotient m∣n < n

I can't think of good names for these though

How about: quotient-| and quotient-<? or else *-divides, *-less-than?

I like quotient-| and quotient-<, better to include the name of the functions involved.

Did we do this?

Nope. Still open.

In the spirit of #1969 you probably also want

baz : ∀ {m n} (m∣n : m ∣ n) → m > 1 → n > m → quotient m∣n > 1

as, say, quotient>1? (the cognate quotient->1 by analogy with the above names, has a bad -> internal symbol clash...)

... and for bar do you also need .{{NonZero n}} as an assumption?

And as a last thought: with the addition of quotient≢0 : .{{NonZero n}} → NonZero quotient to the _∣_ API, a number of arguments about involving possibly-zero quotients might (hopefully) be automatically simplifiable by the typechecker, eg. eliminating this case from Data.Nat.Primality.euclidsLemma