1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/logic.bend as L
4	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
5	import ../natural/arith.bend as NR
6	import ./natfuel.bend as NF
7	
8	# Small Nat lemmas shared by the F64 and the integer (Montgomery, gcd)
9	# proofs. They live here, away from the F64 files, so that importing them
10	# does not re-check the F64 proofs (a Bend import re-checks its file).
11	
12	def dmq(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.add(Nat.mul(Nat.div(x, D), D), Nat.mod(x, D)) == x : Nat}:
13	  match D:
14	    case 0n:
15	      Empty.absurd({Nat.add(Nat.mul(Nat.div(x, 0n), 0n), Nat.mod(x, 0n)) == x : Nat}, N.lt_zero_absurd(0n, hD))
16	    case 1n+ +dp:
17	      Equal.sym(Nat, x, Nat.add(Nat.mul(Nat.div(x, 1n+dp), 1n+dp), Nat.mod(x, 1n+dp)), NR.dm_eq(dp, x))
18	
19	def dml(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.is_lt(Nat.mod(x, D), D) == True{} : Bool}:
20	  match D:
21	    case 0n:
22	      Empty.absurd({Nat.is_lt(Nat.mod(x, 0n), 0n) == True{} : Bool}, N.lt_zero_absurd(0n, hD))
23	    case 1n+ +dp:
24	      NR.dm_lt(dp, x)
25	
26	def mle2(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +hcd: {Nat.is_le(c, d) == True{} : Bool}) -> {Nat.is_le(Nat.mul(a, c), Nat.mul(b, d)) == True{} : Bool}:
27	  +l1 = NF.mul_le_r(a, c, d, hcd)
28	  +l2 = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(d, b)) == True{} : Bool}, Nat.mul(d, a), Nat.mul(a, d), NA.mul_comm(d, a), NF.mul_le_r(d, a, b, hab))
29	  N.le_trans(Nat.mul(a, c), Nat.mul(a, d), Nat.mul(b, d), l1, L.subst(Nat, z => {Nat.is_le(Nat.mul(a, d), z) == True{} : Bool}, Nat.mul(d, b), Nat.mul(b, d), NA.mul_comm(d, b), l2))
30	
31	def mul1(+y: Nat) -> {Nat.mul(1n, y) == y : Nat}:
32	  Equal.trans(Nat, Nat.mul(1n, y), Nat.mul(y, 1n), y, NA.mul_comm(1n, y), NA.mul_one(y))
33	
34	def two_mul(+S: Nat) -> {Nat.mul(S, 2n) == Nat.add(S, S) : Nat}:
35	  Equal.trans(Nat, Nat.mul(S, 2n), Nat.mul(2n, S), Nat.add(S, S), NA.mul_comm(S, 2n), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.mul(1n, S), S, mul1(S)))