blob: 582c8982567aa9b57e38d97a40908b18de08f2f0 [file] [edit]
↑n ^ 2 + m ^ 2 : Int
n ^ 2 + 1 : Nat
↑n ^ 2 + 1 : Int
↑n ^ 2 + ↑1 : Int
q ^ n + 1 : Rat
q ^ m + 1 : Rat
q ^ ↑n + 1 : Rat
12 * q + 1 ≤ 13 * q ^ 2 : Prop
12 * q + 1 ≤ 13 * q ^ 2 : Prop