1	import Base
2	import ../../../spec/math/f64.bend as SF
3	import ./natcmp.bend as NC
4	import ./f64cmp.bend as FC
5	
6	# Small Bool and Nat facts for the F64 square root proofs.
7	
8	def ltz(+l: Nat) -> {Nat.is_lt(0n, l) == Bool.not(Nat.is_eq(l, 0n)) : Bool}:
9	  match l:
10	    case 0n:
11	      {==}
12	    case 1n+ +lp:
13	      {==}
14	
15	def eq_comm(+a: Nat, +b: Nat) -> {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}:
16	  Equal.trans(Bool, Nat.is_eq(a, b), Cmp.is_eq(SF.flip(Nat.cmp(a, b))), Nat.is_eq(b, a), FC.eqflip(Nat.cmp(a, b)), Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), SF.flip(Nat.cmp(a, b)), Nat.cmp(b, a), NC.cmp_flip(a, b)))
17	
18	def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:
19	  match a b:
20	    case True{} True{}:
21	      {==}
22	    case True{} False{}:
23	      {==}
24	    case False{} True{}:
25	      {==}
26	    case False{} False{}:
27	      {==}