Simpler SMT goals

This improves compatibility with Z3 4.13.3 & CVC5 1.1.2

Author: vbgl

theories/algebra/Bigalg.ec

@@ -323,7 +323,8 @@ proof.
 elim: s => // x s IHs F_ge0; rewrite BMul.big_cons. 
 have {IHs} IHs := IHs _; first by smt().
 case: (P x) => [Px F_big_gt0 a a_x_s Pa| nPx /IHs]; 2:smt().
-smt(pmulr_gt0 prodr_ge0_seq).
+rewrite pmulr_gt0 in F_big_gt0; 1, 3:smt().
+apply: prodr_ge0_seq; smt().
 qed.
 
 lemma ler_prod_seq (P : 'a -> bool) (F1 F2 : 'a -> t) s:

theories/datatypes/List.ec

@@ -1133,7 +1133,8 @@ proof.
   move=> s_x; pose i := index x s.
   exists i; exists (drop (i + 1) s ++ take i s).
   rewrite -cat_cons /i /rot => {i}; congr=> //=.
-  elim: s s_x => //= y s IHs; case: (x = y); smt().
+  elim: s s_x=> //= y s IHs; rewrite index_cons.
+  by case: (x = y)=> [<- /= | /#]; rewrite drop0.
 qed.
 
 (* -------------------------------------------------------------------- *)