Improve proofs

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. */

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 */

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 {

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);
       }
     }