This file defines some additional constructive equivalences using
Encodable and the pairing
A noncomputable way to arbitrarily choose an ordering on a finite type.
It is not made into a global instance, since it involves an arbitrary choice.
This can be locally made into an instance with
local attribute [instance] Fintype.toEncodable.
α is finite and all
π a are encodable,
Π a, π a is encodable too. Because the
encoding is not unique, we wrap it in
Trunc to preserve computability.
Outputs the list of differences minus one of the input list, that is
lower' [a₁, a₂, a₃, ...] n = [a₁ - n, a₂ - a₁ - 1, a₃ - a₂ - 1, ...].
Outputs the list of partial sums plus one of the input list, that is
raise [a₁, a₂, a₃, ...] n = [n + a₁, n + a₁ + a₂ + 1, n + a₁ + a₂ + a₃ + 2, ...]. Adding one each
time ensures the elements are distinct.