simplify some smt calls

Author: oskgo

theories/algebra/DynMatrix.eca

@@ -1663,18 +1663,17 @@ lemma catmr_subm m n: 0 <= n < cols m =>
   (subm m 0 (rows m) 0 n || subm m 0 (rows m) n (cols m)) = m.
 proof.
 move => n_bound; rewrite eq_matrixP /=.
-split => [| i j bound]. 
-- smt(rows_catmr cols_catmr size_subm).
+rewrite rows_catmr cols_catmr 2!cols_subm 2!rows_subm /= maxzz /=.
+split => [/#| i j bound]. 
 rewrite get_catmr // cols_subm /=.
 case (j < n) => j_bound.
-- rewrite get_subm /=; first 2 smt(size_catmr size_subm).
-  rewrite (getm0E (subm _ _ _ _ _)).
+- rewrite get_subm /= 1,2:/# (getm0E (subm _ _ _ _ _)).
   + smt(size_catmr size_subm).
   by rewrite addr0.
 - rewrite getm0E; 1: smt(size_catmr size_subm).
   rewrite add0r get_subm; [3:smt()].
-  + smt(rows_catmr rows_subm).
-  + smt(cols_catmr cols_subm).
+  + by elim bound.
+  + smt().
 qed.
 
 lemma subm_colmx (m: matrix) l : 

theories/prelude/Logic.ec

@@ -522,7 +522,7 @@ lemma addbACA : interchange (^) (^)           by smt().
 lemma andb_addl : left_distributive (/\) (^)  by smt().
 lemma andb_addr : right_distributive (/\) (^) by smt().
 lemma addKb : left_loop idfun (^)             by smt().
-lemma addbK : right_loop idfun (^)            by smt().
+lemma addbK : right_loop idfun (^)            by case.
 lemma addIb : left_injective (^)              by smt().
 lemma addbI : right_injective (^)             by smt().