diff --git a/src/probability/martingaleScript.sml b/src/probability/martingaleScript.sml
index 7c6bb4af7c..b8366ee148 100644
--- a/src/probability/martingaleScript.sml
+++ b/src/probability/martingaleScript.sml
@@ -1898,6 +1898,12 @@ Proof
  >> PROVE_TAC [FCP_CONCAT_THM]
 QED
 
+Theorem pair_operation_CONS :
+    pair_operation (\x y. [x; y]) (EL 0) (EL 1)
+Proof
+    rw [pair_operation_def]
+QED
+
 val general_cross_def = Define
    ‘general_cross (cons :'a -> 'b -> 'c) A B = {cons a b | a IN A /\ b IN B}’;
 
@@ -7696,6 +7702,7 @@ Proof
  >> rw [extreal_abs_def]
  >> ‘0 < abs (a + b) /\ 0 < abs a /\ 0 < abs b’ by rw []
  >> rw [normal_powr, extreal_of_num_def, extreal_add_def, extreal_mul_def, extreal_le_eq]
+ >> ONCE_REWRITE_TAC [REAL_MUL_COMM]
  (* below is real-only *)
  >> MATCH_MP_TAC REAL_LE_TRANS
  >> Q.EXISTS_TAC ‘(max (abs a powr r) (abs b powr r)) * 2 powr r’