diff --git a/README.md b/README.md
index 6110705..e26061c 100644
--- a/README.md
+++ b/README.md
@@ -103,10 +103,10 @@ $ ./build.sh
 * [DateDurationSign_year_sign_dominates](theories/Section7/DateDurationSign.v)
 * [CompareISODate_eq_zero](theories/Section3/CompareISODate.v)
 * [CompareISODate_eq_implies_eq_zero](theories/Section3/CompareISODate.v)
+* [CompareTimeRecord_eq_zero](theories/Section4/CompareTimeRecord.v)
 
 ### Unproven
 * [TemporalDateToString_without_calendar_satisfies_rfc3339](theories/Section3/TemporalDateToString.v)
 * [ISODateTimeToString_without_calendar_satisfies_rfc3339](theories/Section5/ISODateTimeToString.v)
 * [AddTime_adding_zero_no_change](theories/Section4/AddTime.v)
-* [CompareTimeRecord_eq_zero](theories/Section4/CompareTimeRecord.v)
 * [CompareTimeRecord_eq_implies_eq_zero](theories/Section4/CompareTimeRecord.v)
diff --git a/theories/Basic.v b/theories/Basic.v
index fb76935..279b9cd 100644
--- a/theories/Basic.v
+++ b/theories/Basic.v
@@ -158,3 +158,5 @@ Proof.
   easy.
   easy.
 Qed.
+
+Lemma zero_le_two : 0 <= 2. Proof. easy. Qed.
diff --git a/theories/Grammar.v b/theories/Grammar.v
index 0c86acc..e822987 100644
--- a/theories/Grammar.v
+++ b/theories/Grammar.v
@@ -49,19 +49,19 @@ Module Grammar.
   Definition Equiv (a b : grammar) := forall s, generates a s <-> generates b s.
 
   Module Equiv.
-    Theorem refl : reflexive grammar Equiv.
+    Lemma refl : reflexive grammar Equiv.
     Proof.
       unfold reflexive, Equiv.
       split; intros; assumption.
     Qed.
 
-    Theorem symm : symmetric grammar Equiv.
+    Lemma symm : symmetric grammar Equiv.
     Proof.
       unfold symmetric, Equiv.
       split; apply H.
     Qed.
 
-    Theorem trans : transitive grammar Equiv.
+    Lemma trans : transitive grammar Equiv.
     Proof.
       unfold transitive, Equiv.
       split.
@@ -76,7 +76,7 @@ Module Grammar.
       as Equiv_rel.
   End Equiv.
 
-  Theorem alternative_assoc :
+  Lemma alternative_assoc :
     forall a b c,
     Equiv (alternative (alternative a b) c) (alternative a (alternative b c)).
   Proof.
@@ -95,7 +95,7 @@ Module Grammar.
         apply gen_alt_r; assumption.
   Qed.
 
-  Theorem alternative_comm :
+  Lemma alternative_comm :
     forall a b, Equiv (alternative a b) (alternative b a).
   Proof.
     split.
@@ -113,7 +113,7 @@ Module Grammar.
         assumption.
   Qed.
 
-  Theorem alternative_nothing : forall a, Equiv a (alternative a nothing).
+  Lemma alternative_nothing : forall a, Equiv a (alternative a nothing).
   Proof.
     split.
     - intros.
@@ -125,7 +125,7 @@ Module Grammar.
       + inversion H.
   Qed.
 
-  Theorem sequence_assoc :
+  Lemma sequence_assoc :
     forall a b c,
     Equiv (sequence (sequence a b) c) (sequence a (sequence b c)).
   Proof.
@@ -146,7 +146,7 @@ Module Grammar.
       + assumption.
   Qed.
 
-  Theorem sequence_empty_l : forall a, Equiv a (sequence empty a).
+  Lemma sequence_empty_l : forall a, Equiv a (sequence empty a).
   Proof.
     split.
     - intros.
@@ -160,7 +160,7 @@ Module Grammar.
       assumption.
   Qed.
 
-  Theorem sequence_empty_r : forall a, Equiv a (sequence a empty).
+  Lemma sequence_empty_r : forall a, Equiv a (sequence a empty).
   Proof.
     split.
     - intros.
@@ -175,7 +175,7 @@ Module Grammar.
       assumption.
   Qed.
 
-  Theorem sequence_nothing_l : forall a, Equiv nothing (sequence nothing a).
+  Lemma sequence_nothing_l : forall a, Equiv nothing (sequence nothing a).
   Proof.
     split.
     - intros.
@@ -185,7 +185,7 @@ Module Grammar.
       inversion H.
   Qed.
 
-  Theorem sequence_nothing_r : forall a, Equiv nothing (sequence a nothing).
+  Lemma sequence_nothing_r : forall a, Equiv nothing (sequence a nothing).
   Proof.
     split.
     - intros.
@@ -195,7 +195,7 @@ Module Grammar.
       inversion H0.
   Qed.
 
-  Theorem unfold_star : forall a, Equiv (star a) (maybe (sequence a (star a))).
+  Lemma unfold_star : forall a, Equiv (star a) (maybe (sequence a (star a))).
   Proof.
     split.
     - intros.
@@ -210,7 +210,7 @@ Module Grammar.
       + apply gen_star_r; assumption.
   Qed.
 
-  Theorem sequence_alternative_distrib_l :
+  Lemma sequence_alternative_distrib_l :
     forall a b c,
     Equiv (sequence a (alternative b c)) (alternative (sequence a b) (sequence a c)).
   Proof.
@@ -234,7 +234,7 @@ Module Grammar.
         assumption.
   Qed.
 
-  Theorem sequence_alternative_distrib_r :
+  Lemma sequence_alternative_distrib_r :
     forall a b c,
     Equiv (sequence (alternative a b) c) (alternative (sequence a c) (sequence b c)).
   Proof.
diff --git a/theories/Section12/ISODaysInMonth.v b/theories/Section12/ISODaysInMonth.v
index f744863..5b0d180 100644
--- a/theories/Section12/ISODaysInMonth.v
+++ b/theories/Section12/ISODaysInMonth.v
@@ -15,7 +15,7 @@ Ltac2 Notation lia := lia0 ().
      month (an integer in the inclusive interval from 1 to 12) and returns a
      positive integer. <<*)
 Definition ISODaysInMonth (year month : Z) (h : 1 <= month <= 12) : Z.
-  ltac1:(refine (
+  refine open_constr:(
     match month as m return (month = m -> Z) with
     (*>> 1. If month is 1, 3, 5, 7, 8, 10, or 12, return 31. <<*)
     | 1 | 3 | 5 | 7 | 8 | 10 | 12 => fun _ => 31
@@ -27,7 +27,7 @@ Definition ISODaysInMonth (year month : Z) (h : 1 <= month <= 12) : Z.
         (*>> 4. Return 28 + MathematicalInLeapYear(EpochTimeForYear(year)). <<*)
         28 + MathematicalInLeapYear (EpochTimeForYear year)
     end eq_refl
-  )).
+  ).
 
   (* Proof of the assert *)
   all: lia.
diff --git a/theories/Section13/DateEquations.v b/theories/Section13/DateEquations.v
index fdce162..c3971f3 100644
--- a/theories/Section13/DateEquations.v
+++ b/theories/Section13/DateEquations.v
@@ -92,7 +92,7 @@ Proof.
       * easy.
 Qed.
 
-Theorem EpochTimeForYear_monotonic :
+Lemma EpochTimeForYear_monotonic :
     forall y0 y1,
     y0 < y1 -> EpochTimeForYear y0 < EpochTimeForYear y1.
 Proof.
@@ -113,14 +113,12 @@ Program Fixpoint FindYearForwards (t y : Z) (h : EpochTimeForYear y < t)
   end.
 
 Next Obligation.
-Proof.
   rewrite <- Z.compare_lt_iff.
   symmetry.
   exact Heq_anonymous.
 Qed.
 
 Next Obligation.
-Proof.
   rewrite <- Z2Nat.inj_lt.
 
   (* t - EpochTimeForYear (y + 1) < t - EpochTimeForYear y *)
@@ -151,14 +149,12 @@ Program Fixpoint FindYearBackwards (t y : Z) (h : t < EpochTimeForYear y)
   end.
 
 Next Obligation.
-Proof.
   rewrite <- Z.compare_lt_iff.
   symmetry.
   exact Heq_anonymous.
 Qed.
 
 Next Obligation.
-Proof.
   rewrite <- Z2Nat.inj_lt.
 
   (* EpochTimeForYear (y - 1) - t < EpochTimeForYear y - t *)
@@ -189,14 +185,12 @@ Program Definition EpochTimeToEpochYear (t : Z) : Z :=
   end.
 
 Next Obligation.
-Proof.
   apply Z.gt_lt.
   symmetry.
   exact Heq_anonymous.
 Qed.
 
 Next Obligation.
-Proof.
   symmetry.
   exact Heq_anonymous.
 Qed.
diff --git a/theories/Section13/FormatTimeString.v b/theories/Section13/FormatTimeString.v
index 2398185..e2b00bf 100644
--- a/theories/Section13/FormatTimeString.v
+++ b/theories/Section13/FormatTimeString.v
@@ -2,6 +2,7 @@ From Stdlib Require Import
   ZArith
   Strings.String.
 From Temporal Require Import
+  Basic
   StringUtil
   Section13.FormatFractionalSeconds
   Section13.PrecisionPrime
diff --git a/theories/Section3/ISODateRecord.v b/theories/Section3/ISODateRecord.v
index 611624e..80ba058 100644
--- a/theories/Section3/ISODateRecord.v
+++ b/theories/Section3/ISODateRecord.v
@@ -17,7 +17,7 @@ Record ISODateRecord : Type :=
   }.
 
 (* This seems to be the case but the spec does not explicitly state it yet. *)
-Theorem ISODateRecord_IsValidISODate :
+Lemma ISODateRecord_IsValidISODate :
   forall (date : ISODateRecord),
   IsValidISODate (year date) (month date) (day date) = true.
 Admitted.
diff --git a/theories/Section3/RegulateISODate.v b/theories/Section3/RegulateISODate.v
index 342631b..a85f8fe 100644
--- a/theories/Section3/RegulateISODate.v
+++ b/theories/Section3/RegulateISODate.v
@@ -47,7 +47,6 @@ Next Obligation. Proof. apply ISODaysInMonth_at_least_1. Qed.
 Next Obligation. Proof. apply clamp_between_lower_and_upper. Qed.
 
 Next Obligation.
-Proof.
   split.
   - apply clamp_between_lower_and_upper.
   - apply clamp_upper_le.
@@ -55,27 +54,23 @@ Proof.
 Qed.
 
 Next Obligation.
-Proof.
   refine (IsValidISODate_month_day_range year _ _ _ _).
   apply clamp_between_lower_and_upper.
 Qed.
 
 Next Obligation.
-Proof.
   destruct overflow.
   - contradiction.
   - reflexivity.
 Qed.
 
 Next Obligation.
-Proof.
   symmetry in Heq_anonymous.
   destruct (IsValidISODate_true year month day Heq_anonymous).
   assumption.
 Qed.
 
 Next Obligation.
-Proof.
   symmetry in Heq_anonymous.
   destruct (IsValidISODate_true year month day Heq_anonymous).
   destruct H.
diff --git a/theories/Section4/AddTime.v b/theories/Section4/AddTime.v
index 1b37dd6..e154f47 100644
--- a/theories/Section4/AddTime.v
+++ b/theories/Section4/AddTime.v
@@ -10,12 +10,9 @@ Definition AddTime (time : TimeRecord) (timeDuration : Z) (timeDuration_valid :
   BalanceTime (hour time) (minute time) (second time) (millisecond time) (microsecond time) (nanosecond time + timeDuration).
   (*>> 2. NOTE: If using floating points to implement this operation, add the time components separately before balancing to avoid errors with unsafe integers. <<*)
 
-Lemma zero_timeDuration_valid :
-  MinTimeDuration <= 0 <= MaxTimeDuration.
+Lemma zero_timeDuration_valid : MinTimeDuration <= 0 <= MaxTimeDuration.
 Proof.
-  split.
-  easy.
-  easy.
+  split; easy.
 Qed.
 
 Theorem AddTime_adding_zero_no_change :
diff --git a/theories/Section4/BalanceTime.v b/theories/Section4/BalanceTime.v
index 7f27664..6ccf337 100644
--- a/theories/Section4/BalanceTime.v
+++ b/theories/Section4/BalanceTime.v
@@ -46,16 +46,14 @@ Program Definition BalanceTime (hour minute second millisecond microsecond nanos
   CreateTimeRecord hour'' minute'' second'' millisecond'' microsecond'' nanosecond' (Some deltaDays) _ _ _ _ _ _ _.
 
 (* DeltaDaysValid (Some deltaDays) *)
-Next Obligation.
-Proof.
-Admitted.
+Next Obligation. Admitted.
 
-Next Obligation. Proof. refine (mod_pos_bound 24 _ _). easy. Qed.
-Next Obligation. Proof. refine (mod_pos_bound 60 _ _). easy. Qed.
-Next Obligation. Proof. refine (mod_pos_bound 60 _ _). easy. Qed.
-Next Obligation. Proof. refine (mod_pos_bound 1000 _ _). easy. Qed.
-Next Obligation. Proof. refine (mod_pos_bound 1000 _ _). easy. Qed.
-Next Obligation. Proof. refine (mod_pos_bound 1000 _ _). easy. Qed.
+Next Obligation. refine (mod_pos_bound 24 _ _). easy. Qed.
+Next Obligation. refine (mod_pos_bound 60 _ _). easy. Qed.
+Next Obligation. refine (mod_pos_bound 60 _ _). easy. Qed.
+Next Obligation. refine (mod_pos_bound 1000 _ _). easy. Qed.
+Next Obligation. refine (mod_pos_bound 1000 _ _). easy. Qed.
+Next Obligation. refine (mod_pos_bound 1000 _ _). easy. Qed.
 
 Lemma mod_if_range :
   forall e u otherwise, 0 < u -> otherwise = true ->
diff --git a/theories/Section4/CompareTimeRecord.v b/theories/Section4/CompareTimeRecord.v
index 693d4c3..08c882b 100644
--- a/theories/Section4/CompareTimeRecord.v
+++ b/theories/Section4/CompareTimeRecord.v
@@ -47,7 +47,12 @@ Proof.
 Qed.
 
 Theorem CompareTimeRecord_eq_zero : forall time, CompareTimeRecord time time = 0.
-Admitted.
+Proof.
+  intros.
+  unfold CompareTimeRecord.
+  repeat (rewrite Z.gtb_ltb, Z.ltb_irrefl).
+  reflexivity.
+Qed.
 
 Theorem CompareTimeRecord_eq_implies_eq_zero :
   forall (d1 d2 h1 h2 m1 m2 s1 s2 ms1 ms2 us1 us2 ns1 ns2 : Z),
diff --git a/theories/Section4/CreateTimeRecord.v b/theories/Section4/CreateTimeRecord.v
index ae08c13..0f57f4d 100644
--- a/theories/Section4/CreateTimeRecord.v
+++ b/theories/Section4/CreateTimeRecord.v
@@ -33,7 +33,6 @@ Program Definition CreateTimeRecord (hour minute second millisecond microsecond
   mkTimeRecord deltaDays' _ hour hour_valid minute minute_valid second second_valid millisecond millisecond_valid microsecond microsecond_valid nanosecond nanosecond_valid.
 
 Next Obligation.
-Proof.
   unfold IsValidTime.
   destruct_with_eqn ((hour <? 0) || (hour >? 23)); try lia.
   destruct_with_eqn ((minute <? 0) || (minute >? 59)); try lia.
@@ -44,7 +43,6 @@ Proof.
 Qed.
 
 Next Obligation.
-Proof.
   destruct deltaDays.
   unfold DeltaDaysValid in days_valid.
   assumption.
diff --git a/theories/Section4/TimeRecord.v b/theories/Section4/TimeRecord.v
index c5ca379..7166f10 100644
--- a/theories/Section4/TimeRecord.v
+++ b/theories/Section4/TimeRecord.v
@@ -33,7 +33,7 @@ Record TimeRecord :=
     nanosecond_valid : 0 <= nanosecond <= 999;
   }.
 
-Theorem TimeRecord_IsValidTime :
+Lemma TimeRecord_IsValidTime :
   forall (t : TimeRecord),
   IsValidTime (hour t) (minute t) (second t) (millisecond t) (microsecond t) (nanosecond t) = true.
 Proof.
diff --git a/theories/Section5/Notes/CombineISODateAndTime.v b/theories/Section5/Notes/CombineISODateAndTime.v
index 6e1f261..2de18a3 100644
--- a/theories/Section5/Notes/CombineISODateAndTime.v
+++ b/theories/Section5/Notes/CombineISODateAndTime.v
@@ -28,6 +28,7 @@ Proof.
   rewrite CompareISODate_eq_zero.
   apply CompareTimeRecord_ignores_days.
 Qed.
+
 Theorem ISODateTimeToString_holds :
   With (fun i0 i1 => ISODateTimeToString i0 = ISODateTimeToString i1).
 Proof.
diff --git a/theories/Section7/DateDurationSign.v b/theories/Section7/DateDurationSign.v
index 391604b..b5e4edf 100644
--- a/theories/Section7/DateDurationSign.v
+++ b/theories/Section7/DateDurationSign.v
@@ -77,7 +77,7 @@ Proof.
   intros.
   unfold DateDurationSign.
   simpl.
-  rewrite <-Z.ltb_lt in H.
+  rewrite <- Z.ltb_lt in H.
   rewrite H.
   reflexivity.
 Qed.
diff --git a/theories/StringUtil.v b/theories/StringUtil.v
index 58f0a65..feb2ae1 100644
--- a/theories/StringUtil.v
+++ b/theories/StringUtil.v
@@ -42,8 +42,6 @@ Definition ToZeroPaddedDecimalString (n minLength : Z) (n_valid : 0 <= n) (minLe
   let S := Z_to_string n in
   StringPad S minLength "0" START minLength_valid.
 
-Lemma zero_le_two : 0 <= 2. Proof. easy. Qed.
-
 Close Scope Z.
 
 Lemma append_assoc :