diff -r 43c2355648d2 -r f2b783abfbe7 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Wed Jan 22 19:17:59 2020 +0000
+++ b/src/HOL/Fun_Def.thy	Mon Jan 27 14:32:43 2020 +0000
@@ -207,6 +207,9 @@
 lemma wf_pair_less[simp]: "wf pair_less"
   by (auto simp: pair_less_def)
 
+lemma total_pair_less [iff]: "total_on A pair_less" and trans_pair_less [iff]: "trans pair_less"
+  by (auto simp: total_on_def pair_less_def)
+
 text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close>
 lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"