ModualrBaseSystem: proved lingering admit in subtraction proof.

2 files changed, 14 insertions, 4 deletions

diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v
index 28ae37233..f0e0db077 100644
--- a/src/Galois/BaseSystem.v
+++ b/src/Galois/BaseSystem.v
@@ -407,6 +407,18 @@ Module BaseSystem (Import B:BaseCoefs).
                                         (apply length_add_ge; omega) .
   Qed.
 
+  Lemma sub_nil_length: forall us : digits, length (sub nil us) = length us.
+  Proof.
+     induction us; boring.
+  Qed.
+
+  Lemma sub_length_le_max : forall us vs,
+      (length (sub us vs) <= max (length us) (length vs))%nat.
+  Proof.
+    induction us, vs; boring.
+    rewrite sub_nil_length; auto.
+  Qed.
+
   Lemma mul_bi_length : forall us n, length (mul_bi n us) = (length us + n)%nat.
   Proof.
     pose proof mul_bi'_length; unfold mul_bi.
diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v
index 138eabd3f..b0b8e1495 100644
--- a/src/Galois/ModularBaseSystem.v
+++ b/src/Galois/ModularBaseSystem.v
@@ -258,10 +258,8 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
   Lemma sub_rep : forall u v x y, u ~= x -> v ~= y -> sub u v ~= (x-y)%GF.
   Proof.
     autounfold; intuition. {
-      (*unfold add.
-      rewrite B.add_length_le_max.
-      B.case_max; try rewrite Max.max_r; omega.*)
-      admit.
+      rewrite B.sub_length_le_max.
+      case_max; try rewrite Max.max_r; omega.
     }
     unfold toGF in *; unfold B.decode in *.
     rewrite B.sub_rep.