diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
index 472917014f..a945bf26f7 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
index e42777eee0..82f1dd9c04 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
index 4c1f17a2c9..c10fa53897 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
index a7e521f03b..0833926024 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
index a1da869938..fdf2bb7c73 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
index e823114e53..17a311f71f 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
index 66b9992996..6b731da1c4 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo differ
diff --git a/Source/DafnyStandardLibraries/src/Std/Arithmetic/LittleEndianNat.dfy b/Source/DafnyStandardLibraries/src/Std/Arithmetic/LittleEndianNat.dfy
index 79da13c75d..a5a99c223a 100644
--- a/Source/DafnyStandardLibraries/src/Std/Arithmetic/LittleEndianNat.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/Arithmetic/LittleEndianNat.dfy
@@ -122,8 +122,17 @@ abstract module {:disableNonlinearArithmetic} Std.Arithmetic.LittleEndianNat {
     requires |xs| == 2
     ensures ToNatRight(xs) == First(xs) + xs[1] * BASE()
   {
-    reveal ToNatRight();
-    LemmaSeqLen1(DropLast(xs));
+    var xs1 := DropFirst(xs);
+    assert DropFirst(xs1) == [];
+    calc {
+      ToNatRight(xs);
+      { reveal ToNatRight(); }
+      ToNatRight(xs1) * BASE() + First(xs);
+      { reveal ToNatRight(); }
+      (ToNatRight([]) * BASE() + First(xs1)) * BASE() + First(xs);
+      { reveal ToNatRight(); }
+      (0 * BASE() + First(xs1)) * BASE() + First(xs);
+    }
   }
 
   /* Appending a zero does not change the nat representation of the sequence. */
diff --git a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy
index 8731e740e2..d6dc6d9b40 100644
--- a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy
@@ -41,8 +41,21 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.Mul {
     requires x >= 0
     ensures x * y == MulPos(x, y)
   {
-    reveal MulPos();
-    LemmaMulInductionAuto(x, u => u >= 0 ==> u * y == MulPos(u, y));
+    if x == 0 {
+      assert MulPos(x, y) == 0 by {
+        reveal MulPos();
+      }
+    } else {
+      calc {
+        MulPos(x, y);
+        { reveal MulPos(x, y); }
+        y + MulPos(x - 1, y);
+        { LemmaMulIsMulPos(x - 1, y); }
+        y + (x - 1) * y;
+        { LemmaMulDistributes(); }
+        x * y;
+      }
+    }
   }
 
   /* ensures that the basic properties of multiplication, including the identity and zero properties */
diff --git a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Power.dfy b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Power.dfy
index e8c99e338a..62419d5ea8 100644
--- a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Power.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Power.dfy
@@ -417,9 +417,8 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.Power {
     ensures Pow(b, e1) <= Pow(b, e2)
   {
     reveal Pow();
-    LemmaPowAuto();
     var f := e => 0 <= e ==> Pow(b, e1) <= Pow(b, e1 + e);
-    forall i {:trigger IsLe(0, i)} | IsLe(0, i) && f(i)
+    forall i | IsLe(0, i) && f(i)
       ensures f(i + 1)
     {
       calc {
diff --git a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
index eaddebc3a3..7dbfe3c42c 100644
--- a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
@@ -781,10 +781,10 @@ module Std.Collections.Seq {
   /* Filtering a sequence is distributive over concatenation. That is, concatenating two sequences
      and then using "Filter" is the same as using "Filter" on each sequence separately, and then
      concatenating the two resulting sequences. */
-  lemma {:isolate_assertions}
-  LemmaFilterDistributesOverConcat<T(!new)>(f: (T ~> bool), xs: seq<T>, ys: seq<T>)
-    requires forall i {:trigger xs[i]}:: 0 <= i < |xs| ==> f.requires(xs[i])
-    requires forall j {:trigger ys[j]}:: 0 <= j < |ys| ==> f.requires(ys[j])
+  lemma {:isolate_assertions} {:induction false}
+  LemmaFilterDistributesOverConcat<T(!new)>(f: T ~> bool, xs: seq<T>, ys: seq<T>)
+    requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
+    requires forall j :: 0 <= j < |ys| ==> f.requires(ys[j])
     ensures Filter(f, xs + ys) == Filter(f, xs) + Filter(f, ys)
   {
     reveal Filter();
@@ -793,10 +793,11 @@ module Std.Collections.Seq {
     } else {
       calc {
         Filter(f, xs + ys);
-        { assert {:split_here} (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; }
+        { assert (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; }
         Filter(f, [xs[0]]) + Filter(f, xs[1..] + ys);
+        { LemmaFilterDistributesOverConcat(f, xs[1..], ys); }
         Filter(f, [xs[0]]) + (Filter(f, xs[1..]) + Filter(f, ys));
-        { assert {:split_here} [(xs + ys)[0]] + (xs[1..] + ys) == xs + ys; }
+        { assert [(xs + ys)[0]] + (xs[1..] + ys) == xs + ys; }
         Filter(f, xs) + Filter(f, ys);
       }
     }