law qg1
lawful-fields@0.1.1.0 · proof_num.bend:92
import lawful-fields@0.1.1.0/proof_num.bend as ProofNum
import Base
92law qg1:
93 for +N1: Nat
94 for +Qn: Nat
95 for +R: Nat
96 for +T: Nat
97 for +M: Nat
98 for +hdm: {Nat.add(Nat.mul(Nat.div(N1, T), T), Nat.mod(N1, T)) == N1 : Nat}
99 for +hd: {Nat.div(N1, T) == Qn : Nat}
100 for +hr: {Nat.mod(N1, T) == R : Nat}
101 for +hT: {T == 10n : Nat}
102 for +hR: {R == 5n : Nat}
103 for +eN: {N1 == Nat.sub(M, 1n) : Nat}
104 {Nat.add(Nat.mul(Qn, 10n), 5n) == Nat.sub(M, 1n) : Nat}