remove more holes

base/Nat/Order.kind

@@ -208,26 +208,6 @@ Nat.Order.add.combine(
   let right_lem = Nat.Order.add.left(c, d, b, Hyp1)
   let qed = Nat.Order.chain(Nat.add(a, c), Nat.add(b, c), Nat.add(b,d), left_lem, right_lem)
   qed
-//  left_lem = Nat.Order.add.right!!(c, Hyp0)
-//  right_lem = Nat.Order.add.left!!(b, Hyp1)
-//  qed = Nat.Order.chain!!!(left_lem, right_lem)
-//  qed
-
-Nat.Order.mul.right(
-  a: Nat
-  b: Nat
-  c: Nat
-  Hyp: Equal<Bool>(Nat.lte(a, b), true)
-): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true)
-  // TODO
-  case c {
-    zero:
-      Equal.refl<Bool>(true)
-    succ:
-      let ind = Nat.Order.mul.right(a, b, c.pred, Hyp)
-      let qed = Nat.Order.add.combine(a, b, Nat.mul(a,c.pred), Nat.mul(b,c.pred), Hyp, ind)
-      qed
-  }: Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true)
 
 Nat.Order.mul.left(
   a: Nat
@@ -236,20 +216,32 @@ Nat.Order.mul.left(
   Hyp: Equal<Bool>(Nat.lte(a, b), Bool.true)
 ): Equal<Bool>(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), Bool.true)
   // TODO
-  let lem = Nat.Order.mul.right(a, b, c, Hyp)
+  case c {
+    zero:
+      Equal.refl<Bool>(true)
+    succ:
+      let ind = Nat.Order.mul.left(a, b, c.pred, Hyp)
+      let qed = Nat.Order.add.combine(a, b, Nat.mul(c.pred,a),Nat.mul(c.pred,b), Hyp, ind)
+      qed
+  }: Equal<Bool>(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), true)
+
+
+Nat.Order.mul.right(
+  a: Nat
+  b: Nat
+  c: Nat
+  Hyp: Equal<Bool>(Nat.lte(a, b), true)
+): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true)
+  let lem = Nat.Order.mul.left(a, b, c, Hyp)
   let lem = Equal.rewrite<Nat>(
-    Nat.mul(a, c), Nat.mul(c, a), Nat.mul.comm(a, c),
-    (x) Equal<Bool>(Nat.lte(x, Nat.mul(b, c)), Bool.true), lem
+    Nat.mul(c,a), Nat.mul(a, c), Nat.mul.comm(c, a)
+    (x) Equal<Bool>(Nat.lte(x, Nat.mul(c, b)), Bool.true), lem
   )
   let qed = Equal.rewrite<Nat>(
-    Nat.mul(b, c), Nat.mul(c, b), Nat.mul.comm(b, c),
-    (x) Equal<Bool>(Nat.lte(Nat.mul(c, a), x), Bool.true), lem
+    Nat.mul(c, b), Nat.mul(b, c), Nat.mul.comm(c, b)
+    (x) Equal<Bool>(Nat.lte(Nat.mul(a, c), x), Bool.true), lem
   )
   qed
-//  lem = Nat.Order.mul.right(a, b, c, Hyp)
-//  lem = lem :: rewrite X in Nat.lte(X, Nat.mul(b, c)) == true with Nat.mul.comm(a, c)
-//  qed = lem :: rewrite X in Nat.lte(Nat.mul(c, a), X) == true with Nat.mul.comm(b, c)
-//  qed
 
 Nat.Order.mul.combine(
   a: Nat,

base/Nat/add/cancel_right.kind

@@ -2,6 +2,15 @@
 Nat.add.cancel_right(
   a: Nat, b: Nat, c: Nat, h: Equal<Nat>(Nat.add(a, b), Nat.add(c, b))
 ): Equal<Nat>(a, c)
-  let h1 = h  :: rewrite x in x == Nat.add(c,b) with Nat.add.comm(a, b)
-  let h2 = h1 :: rewrite x in Nat.add(b,a) == x with Nat.add.comm(c, b)
-  Nat.add.cancel_left(_ _ _ h2)
+  let lemma = Equal.rewrite<Nat>(
+    Nat.add(a,b), Nat.add(b,a), Nat.add.comm(a, b),
+    (x) Equal<Nat>(x, Nat.add(c, b))
+    h
+  )
+  let lemma = Equal.rewrite<Nat>(
+    Nat.add(c,b), Nat.add(b,c), Nat.add.comm(c, b),
+    (x) Equal<Nat>(Nat.add(b, a), x)
+    lemma
+  )
+  let qed = Nat.add.cancel_left(b, a, c, lemma)
+  qed

base/Nat/add/comm.kind

@@ -1,13 +1,26 @@
-Nat.add.comm(a: Nat, b:Nat): (a + b) == (b + a)
-  case a{
-    zero: mirror(Nat.add.zero_right(b))
+Nat.add.comm(
+  a: Nat, b:Nat
+): Equal<Nat>(Nat.add(a, b), Nat.add(b, a))
+  case a {
+    zero:
+      Equal.mirror<Nat>(
+        Nat.add(b,0), b
+        Nat.add.zero_right(b)
+      )
     succ: 
-      let p0 = Nat.add.succ_right(b, a.pred)
-      let p1 = mirror(p0)
-      let h2 = Nat.add.comm(b, a.pred)
-      let p3 = p1 :: rewrite x in Nat.succ(x) == Nat.add(b,Nat.succ(a.pred)) with h2
-      // here p3 should close the goal.
-      let p4 = mirror(Nat.add.succ_left(a.pred,b))
-      let p5 = p3 :: rewrite x in x == _ with p4
-      p5
-  }!
+      let ind = Nat.add.comm(a.pred, b)
+      let lemma = Equal.apply<Nat, Nat>(
+        Nat.add(a.pred,b), Nat.add(b,a.pred)
+        Nat.succ, ind
+      )
+      let succ_right = Equal.mirror<Nat>(
+        Nat.add(b,Nat.succ(a.pred)), Nat.succ(Nat.add(b,a.pred))
+        Nat.add.succ_right(b, a.pred)
+      )
+      let qed = Equal.rewrite<Nat>(
+        Nat.succ(Nat.add(b,a.pred)), Nat.add(b,Nat.succ(a.pred)), succ_right
+        (x) Equal<Nat>(Nat.add(Nat.succ(a.pred), b), x)
+        lemma
+      )
+      qed
+  }: Equal<Nat>(Nat.add(a, b), Nat.add(b, a))

base/Nat/add/succ_both.kind

@@ -1,5 +1,6 @@
-Nat.add.succ_both(a: Nat, b: Nat)
-: (Nat.succ(a) + Nat.succ(b)) == Nat.succ(Nat.succ(a + b))
+Nat.add.succ_both(
+  a: Nat, b: Nat
+): (Nat.succ(a) + Nat.succ(b)) == Nat.succ(Nat.succ(a + b))
   case a {
     zero: refl
     succ: apply(Nat.succ, Nat.add.succ_both(a.pred, b))