[STATEMENT]
lemma limit_mat_denote_while_n:
  assumes wc: "well_com (While M S)" and dr: "\<rho> \<in> carrier_mat d d" and pdor: "partial_density_operator \<rho>"
  shows "limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have m: "measurement d 2 M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measurement d 2 M
[PROOF STEP]
using wc
[PROOF STATE]
proof (prove)
using this:
well_com (While M S)

goal (1 subgoal):
 1. measurement d 2 M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
measurement d 2 M

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
measurement d 2 M
[PROOF STEP]
have dM0: "M 0 \<in> carrier_mat d d" and dM1: "M 1 \<in> carrier_mat d d" and id: "adjoint (M 0) * (M 0) + adjoint (M 1) * (M 1) = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
using this:
measurement d 2 M

goal (1 subgoal):
 1. M 0 \<in> carrier_mat d d &&& M 1 \<in> carrier_mat d d &&& adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m d
[PROOF STEP]
using measurement_id2 m measurement_def
[PROOF STATE]
proof (prove)
using this:
measurement d 2 M
measurement ?d 2 ?M \<Longrightarrow> adjoint (?M 0) * ?M 0 + adjoint (?M 1) * ?M 1 = 1\<^sub>m ?d
measurement d 2 M
measurement ?d ?n ?M = ((\<forall>j<?n. ?M j \<in> carrier_mat ?d ?d) \<and> matrix_sum ?d (\<lambda>j. adjoint (?M j) * ?M j) ?n = 1\<^sub>m ?d)

goal (1 subgoal):
 1. M 0 \<in> carrier_mat d d &&& M 1 \<in> carrier_mat d d &&& adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M 0 \<in> carrier_mat d d
M 1 \<in> carrier_mat d d
adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m d

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have wcs: "well_com S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_com S
[PROOF STEP]
using wc
[PROOF STATE]
proof (prove)
using this:
well_com (While M S)

goal (1 subgoal):
 1. well_com S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_com S

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have DS: "positive (denote S \<rho>) \<and> trace (denote S \<rho>) \<le> trace \<rho> \<and> denote S \<rho> \<in> carrier_mat d d"
    if "\<rho> \<in> carrier_mat d d" and "partial_density_operator \<rho>" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (denote S \<rho>) \<and> trace (denote S \<rho>) \<le> trace \<rho> \<and> denote S \<rho> \<in> carrier_mat d d
[PROOF STEP]
using wcs that denote_positive_trace_dim
[PROOF STATE]
proof (prove)
using this:
well_com S
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<lbrakk>well_com ?S; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?S ?\<rho>) \<and> trace (denote ?S ?\<rho>) \<le> trace ?\<rho> \<and> denote ?S ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote S \<rho>) \<and> trace (denote S \<rho>) \<le> trace \<rho> \<and> denote S \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote S ?\<rho>) \<and> trace (denote S ?\<rho>) \<le> trace ?\<rho> \<and> denote S ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have sumdd: "(\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n \<in> carrier_mat d d)"
    if "\<rho> \<in> carrier_mat d d" and "partial_density_operator \<rho>" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_sum_dim dM0 dM1 DS that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; ?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; partial_density_operator ?\<rho>; \<And>\<rho>'. \<lbrakk>\<rho>' \<in> carrier_mat d d; partial_density_operator \<rho>'\<rbrakk> \<Longrightarrow> positive (?DS \<rho>') \<and> trace (?DS \<rho>') \<le> trace \<rho>' \<and> ?DS \<rho>' \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n \<in> carrier_mat d d
M 0 \<in> carrier_mat d d
M 1 \<in> carrier_mat d d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote S ?\<rho>) \<and> trace (denote S ?\<rho>) \<le> trace ?\<rho> \<and> denote S ?\<rho> \<in> carrier_mat d d
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have sumtr: "\<forall> n. trace (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n) \<le> trace \<rho>"
    if "\<rho> \<in> carrier_mat d d" and "partial_density_operator \<rho>" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
using denote_while_n_sum_trace[OF dM0 dM1 id DS] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<in> carrier_mat d d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> partial_density_operator \<rho>; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) ?n) \<le> trace ?\<rho>
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. \<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) n) \<le> trace ?\<rho>

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have sumpar: "(\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n))"
    if "\<rho> \<in> carrier_mat d d" and "partial_density_operator \<rho>" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n)
[PROOF STEP]
using denote_while_n_sum_partial_density[OF dM0 dM1 id DS] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<in> carrier_mat d d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> partial_density_operator \<rho>; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) ?n)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) n)

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have sumle:"(\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) (Suc n))"
    if "\<rho> \<in> carrier_mat d d" and "partial_density_operator \<rho>" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) (Suc n)
[PROOF STEP]
using denote_while_n_sum_lowner_le[OF dM0 dM1 id DS] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<in> carrier_mat d d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> partial_density_operator \<rho>; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) ?n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) (Suc ?n)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>) (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) (Suc n)

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have seqd: "matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>))"
    if "\<rho> \<in> carrier_mat d d" and "partial_density_operator \<rho>" for \<rho>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>))
[PROOF STEP]
using matrix_seq_def sumdd sumpar sumle that
[PROOF STATE]
proof (prove)
using this:
matrix_seq ?dim ?f \<equiv> (\<forall>n. ?f n \<in> carrier_mat ?dim ?dim) \<and> (\<forall>n. partial_density_operator (?f n)) \<and> (\<forall>n. ?f n \<le>\<^sub>L ?f (Suc n))
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) n \<in> carrier_mat d d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) n)
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>) (Suc n)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n ?\<rho>))

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
have "matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>))
    (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)))
[PROOF STEP]
using DS lowner_is_lub_matrix_sum dM0 dM1 id pdor dr
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote S ?\<rho>) \<and> trace (denote S ?\<rho>) \<le> trace ?\<rho> \<and> denote S ?\<rho> \<in> carrier_mat d d
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>)))
M 0 \<in> carrier_mat d d
M 1 \<in> carrier_mat d d
adjoint (M 0) * M 0 + adjoint (M 1) * M 1 = 1\<^sub>m d
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)))

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)))
[PROOF STEP]
show "limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d"
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)))

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d
[PROOF STEP]
unfolding denote.simps denote_while_def matrix_inf_sum_def
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)))

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>))) d
[PROOF STEP]
using matrix_seq.lowner_lub_is_limit[OF seqd[OF dr pdor]]
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_is_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)))
limit_mat (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>))) d

goal (1 subgoal):
 1. limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (M 0) (M 1) (denote S) n \<rho>))) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (matrix_sum d (\<lambda>k. denote_while_n (M 0) (M 1) (denote S) k \<rho>)) (denote (While M S) \<rho>) d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convex_bound_le:
  assumes "x \<le> a" and "y \<le> a" and "0 \<le> u" and "0 \<le> v" and "u + v = 1"
  shows "u * x + v * y \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u * x + v * y \<le> a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u * x + v * y \<le> a
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<le> a
y \<le> a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)
[PROOF STEP]
have "u * x + v * y \<le> u * a + v * a"
[PROOF STATE]
proof (prove)
using this:
x \<le> a
y \<le> a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)

goal (1 subgoal):
 1. u * x + v * y \<le> u * a + v * a
[PROOF STEP]
by (simp add: add_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
u * x + v * y \<le> u * a + v * a

goal (1 subgoal):
 1. u * x + v * y \<le> a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x \<le> a
y \<le> a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)
u * x + v * y \<le> u * a + v * a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> a
y \<le> a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)
u * x + v * y \<le> u * a + v * a

goal (1 subgoal):
 1. u * x + v * y \<le> a
[PROOF STEP]
unfolding distrib_right[symmetric]
[PROOF STATE]
proof (prove)
using this:
x \<le> a
y \<le> a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)
u * x + v * y \<le> (u + v) * a

goal (1 subgoal):
 1. u * x + v * y \<le> a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u * x + v * y \<le> a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; (0::'a) < b\<rbrakk> \<Longrightarrow> (0::'a) < a * b
[PROOF STEP]
using mult_strict_left_mono [of 0 b a]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) < b; (0::'a) < a\<rbrakk> \<Longrightarrow> a * (0::'a) < a * b

goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; (0::'a) < b\<rbrakk> \<Longrightarrow> (0::'a) < a * b
[PROOF STEP]
by simp


[STATEMENT]
lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; b < (0::'a)\<rbrakk> \<Longrightarrow> a * b < (0::'a)
[PROOF STEP]
using mult_strict_left_mono [of b 0 a]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b < (0::'a); (0::'a) < a\<rbrakk> \<Longrightarrow> a * b < a * (0::'a)

goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; b < (0::'a)\<rbrakk> \<Longrightarrow> a * b < (0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < (0::'a); (0::'a) < b\<rbrakk> \<Longrightarrow> a * b < (0::'a)
[PROOF STEP]
using mult_strict_right_mono [of a 0 b]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < (0::'a); (0::'a) < b\<rbrakk> \<Longrightarrow> a * b < (0::'a) * b

goal (1 subgoal):
 1. \<lbrakk>a < (0::'a); (0::'a) < b\<rbrakk> \<Longrightarrow> a * b < (0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma mult_strict_mono:
  assumes t1: "a < b" and t2: "c < d" and t3: "0 < b" and t4: "0 \<le> c"
  shows "a * c < b * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
have "a * c < b * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
by (metis local.dual_order.order_iff_strict local.dual_order.strict_trans2
        local.mult_strict_left_mono local.mult_strict_right_mono local.mult_zero_right t1 t2 t3 t4)
[PROOF STATE]
proof (state)
this:
a * c < b * d

goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a * c < b * d

goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a * c < b * d
a < b
c < d
(0::'a) < b
(0::'a) \<le> c

goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a * c < b * d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_strict_mono':
  assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
  shows "a * c < b * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
by (rule mult_strict_mono) (insert assms, auto)


[STATEMENT]
lemma mult_less_le_imp_less:
  assumes t1: "a < b" and t2: "c \<le> d" and t3: "0 \<le> a" and t4: "0 < c"
  shows "a * c < b * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
using local.mult_strict_mono' local.mult_strict_right_mono local.order.order_iff_strict
    t1 t2 t3 t4
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < ?b; ?c < ?d; (0::'a) \<le> ?a; (0::'a) \<le> ?c\<rbrakk> \<Longrightarrow> ?a * ?c < ?b * ?d
\<lbrakk>?a < ?b; (0::'a) < ?c\<rbrakk> \<Longrightarrow> ?a * ?c < ?b * ?c
(?a \<le> ?b) = (?a < ?b \<or> ?a = ?b)
a < b
c \<le> d
(0::'a) \<le> a
(0::'a) < c

goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_le_less_imp_less:
  assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
  shows "a * c < b * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * c < b * d
[PROOF STEP]
by (metis assms(1) assms(2) assms(3) assms(4) local.antisym_conv2 local.dual_order.strict_trans1
      local.mult_strict_left_mono local.mult_strict_mono)


[STATEMENT]
lemma convex_bound_lt:
  assumes "x < a" and "y < a" and "0 \<le> u" and "0 \<le> v" and "u + v = 1"
  shows "u * x + v * y < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u * x + v * y < a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u * x + v * y < a
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x < a
y < a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)
[PROOF STEP]
have "u * x + v * y < u * a + v * a"
[PROOF STATE]
proof (prove)
using this:
x < a
y < a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)

goal (1 subgoal):
 1. u * x + v * y < u * a + v * a
[PROOF STEP]
by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
u * x + v * y < u * a + v * a

goal (1 subgoal):
 1. u * x + v * y < a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x < a
y < a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)
u * x + v * y < u * a + v * a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < a
y < a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)
u * x + v * y < u * a + v * a

goal (1 subgoal):
 1. u * x + v * y < a
[PROOF STEP]
unfolding distrib_right[symmetric]
[PROOF STATE]
proof (prove)
using this:
x < a
y < a
(0::'a) \<le> u
(0::'a) \<le> v
u + v = (1::'a)
u * x + v * y < (u + v) * a

goal (1 subgoal):
 1. u * x + v * y < a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u * x + v * y < a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < a; c < (0::'a)\<rbrakk> \<Longrightarrow> c * a < c * b
[PROOF STEP]
using mult_strict_left_mono [of b a "- c"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b < a; (0::'a) < - c\<rbrakk> \<Longrightarrow> - c * b < - c * a

goal (1 subgoal):
 1. \<lbrakk>b < a; c < (0::'a)\<rbrakk> \<Longrightarrow> c * a < c * b
[PROOF STEP]
by simp


[STATEMENT]
lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < a; c < (0::'a)\<rbrakk> \<Longrightarrow> a * c < b * c
[PROOF STEP]
using mult_strict_right_mono [of b a "- c"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b < a; (0::'a) < - c\<rbrakk> \<Longrightarrow> b * - c < a * - c

goal (1 subgoal):
 1. \<lbrakk>b < a; c < (0::'a)\<rbrakk> \<Longrightarrow> a * c < b * c
[PROOF STEP]
by simp


[STATEMENT]
lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < (0::'a); b < (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) < a * b
[PROOF STEP]
using mult_strict_right_mono_neg [of a 0 b]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < (0::'a); b < (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) * b < a * b

goal (1 subgoal):
 1. \<lbrakk>a < (0::'a); b < (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) < a * b
[PROOF STEP]
by simp


[STATEMENT]
lemma frac_less_eq:
  "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z - w * y) / (y * z) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> (0::'a); z \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (x / y < w / z) = ((x * z - w * y) / (y * z) < (0::'a))
[PROOF STEP]
by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )


[STATEMENT]
lemma frac_le_eq:
  "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> (0::'a); z \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (x / y \<le> w / z) = ((x * z - w * y) / (y * z) \<le> (0::'a))
[PROOF STEP]
by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )


[STATEMENT]
lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a \<longleftrightarrow> a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) = (1::'a) / a) = (a = (0::'a))
[PROOF STEP]
by (cases "a = 0") (auto simp: field_simps)


[STATEMENT]
lemma one_divide_eq_0_iff [simp]: "1 / a = 0 \<longleftrightarrow> a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) / a = (0::'a)) = (a = (0::'a))
[PROOF STEP]
using zero_eq_1_divide_iff[of a]
[PROOF STATE]
proof (prove)
using this:
((0::'a) = (1::'a) / a) = (a = (0::'a))

goal (1 subgoal):
 1. ((1::'a) / a = (0::'a)) = (a = (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma eq_divide_eq_1 [simp]:
  "(1 = b/a) = ((a \<noteq> 0 & a = b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) = b / a) = (a \<noteq> (0::'a) \<and> a = b)
[PROOF STEP]
by (auto simp add: eq_divide_eq)


[STATEMENT]
lemma divide_eq_eq_1 [simp]:
  "(b/a = 1) = ((a \<noteq> 0 & a = b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b / a = (1::'a)) = (a \<noteq> (0::'a) \<and> a = b)
[PROOF STEP]
by (auto simp add: divide_eq_eq)


[STATEMENT]
lemma comparable:
  assumes h1: "a \<le> c \<or> a \<ge> c"
    and h2: "b \<le> c \<or> b \<ge> c"
  shows "a \<le> b \<or> b \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
have "a \<le> b"
    if t1: "\<not> b \<le> a" and t2: "a \<le> c" and t3: "b \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
have "0 \<le> c-a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> c - a
[PROOF STEP]
by (simp add: t2)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> c - a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> c - a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
have "0 \<le> c-b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> c - b
[PROOF STEP]
by (simp add: t3)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> c - b

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> c - a
(0::'a) \<le> c - b
[PROOF STEP]
have "c-a \<le> c-b \<or> c-a \<ge> c-b"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> c - a
(0::'a) \<le> c - b

goal (1 subgoal):
 1. c - a \<le> c - b \<or> c - b \<le> c - a
[PROOF STEP]
by (rule nn_comparable)
[PROOF STATE]
proof (state)
this:
c - a \<le> c - b \<or> c - b \<le> c - a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
hence "-a \<le> -b \<or> -a \<ge> -b"
[PROOF STATE]
proof (prove)
using this:
c - a \<le> c - b \<or> c - b \<le> c - a

goal (1 subgoal):
 1. - a \<le> - b \<or> - b \<le> - a
[PROOF STEP]
using local.add_le_imp_le_right local.uminus_add_conv_diff
[PROOF STATE]
proof (prove)
using this:
c - a \<le> c - b \<or> c - b \<le> c - a
?a + ?c \<le> ?b + ?c \<Longrightarrow> ?a \<le> ?b
- ?a + ?b = ?b - ?a

goal (1 subgoal):
 1. - a \<le> - b \<or> - b \<le> - a
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
- a \<le> - b \<or> - b \<le> - a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
- a \<le> - b \<or> - b \<le> - a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
by (simp add: t1)
[PROOF STATE]
proof (state)
this:
a \<le> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> b \<le> a; a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b

goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> b \<le> a; a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b

goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
have "a \<le> b"
    if t1: "\<not> b \<le> a" and t2: "c \<le> a" and t3: "b \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
have "b \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> a
[PROOF STEP]
using local.dual_order.trans t2 t3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
c \<le> a
b \<le> c

goal (1 subgoal):
 1. b \<le> a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b \<le> a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<le> a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
using t1
[PROOF STATE]
proof (prove)
using this:
b \<le> a
\<not> b \<le> a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> b \<le> a; c \<le> a; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b

goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> b \<le> a; c \<le> a; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b

goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
have "a \<le> b"
    if t1: "\<not> b \<le> a" and t2: "c \<le> a" and t3: "c \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
have "0 \<le> a-c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> a - c
[PROOF STEP]
by (simp add: t2)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a - c

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a - c

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
have "0 \<le> b-c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> b - c
[PROOF STEP]
by (simp add: t3)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> b - c

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> a - c
(0::'a) \<le> b - c
[PROOF STEP]
have "a-c \<le> b-c \<or> a-c \<ge> b-c"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a - c
(0::'a) \<le> b - c

goal (1 subgoal):
 1. a - c \<le> b - c \<or> b - c \<le> a - c
[PROOF STEP]
by (rule nn_comparable)
[PROOF STATE]
proof (state)
this:
a - c \<le> b - c \<or> b - c \<le> a - c

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
hence "a \<le> b \<or> a \<ge> b"
[PROOF STATE]
proof (prove)
using this:
a - c \<le> b - c \<or> b - c \<le> a - c

goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
by (simp add: local.le_diff_eq)
[PROOF STATE]
proof (state)
this:
a \<le> b \<or> b \<le> a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> b \<or> b \<le> a

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
by (simp add: t1)
[PROOF STATE]
proof (state)
this:
a \<le> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> b \<le> a; c \<le> a; c \<le> b\<rbrakk> \<Longrightarrow> a \<le> b

goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> b \<le> a; a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b
\<lbrakk>\<not> b \<le> a; c \<le> a; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b
\<lbrakk>\<not> b \<le> a; c \<le> a; c \<le> b\<rbrakk> \<Longrightarrow> a \<le> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> b \<le> a; a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b
\<lbrakk>\<not> b \<le> a; c \<le> a; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b
\<lbrakk>\<not> b \<le> a; c \<le> a; c \<le> b\<rbrakk> \<Longrightarrow> a \<le> b

goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> b \<le> a; a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b
\<lbrakk>\<not> b \<le> a; c \<le> a; b \<le> c\<rbrakk> \<Longrightarrow> a \<le> b
\<lbrakk>\<not> b \<le> a; c \<le> a; c \<le> b\<rbrakk> \<Longrightarrow> a \<le> b
a \<le> c \<or> c \<le> a
b \<le> c \<or> c \<le> b

goal (1 subgoal):
 1. a \<le> b \<or> b \<le> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> b \<or> b \<le> a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma negative_imp_inverse_negative:
  "a < 0 \<Longrightarrow> inverse a < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < (0::'a) \<Longrightarrow> inverse a < (0::'a)
[PROOF STEP]
by (insert positive_imp_inverse_positive [of "-a"],
      simp add: nonzero_inverse_minus_eq less_imp_not_eq)


[STATEMENT]
lemma inverse_positive_imp_positive:
  assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
  shows "0 < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) < a
[PROOF STEP]
have "0 < inverse (inverse a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < inverse (inverse a)
[PROOF STEP]
using inv_gt_0
[PROOF STATE]
proof (prove)
using this:
(0::'a) < inverse a

goal (1 subgoal):
 1. (0::'a) < inverse (inverse a)
[PROOF STEP]
by (rule positive_imp_inverse_positive)
[PROOF STATE]
proof (state)
this:
(0::'a) < inverse (inverse a)

goal (1 subgoal):
 1. (0::'a) < a
[PROOF STEP]
thus "0 < a"
[PROOF STATE]
proof (prove)
using this:
(0::'a) < inverse (inverse a)

goal (1 subgoal):
 1. (0::'a) < a
[PROOF STEP]
using nz
[PROOF STATE]
proof (prove)
using this:
(0::'a) < inverse (inverse a)
a \<noteq> (0::'a)

goal (1 subgoal):
 1. (0::'a) < a
[PROOF STEP]
by (simp add: nonzero_inverse_inverse_eq)
[PROOF STATE]
proof (state)
this:
(0::'a) < a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inverse_negative_imp_negative:
  assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
  shows "a < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < (0::'a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a < (0::'a)
[PROOF STEP]
have "inverse (inverse a) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (inverse a) < (0::'a)
[PROOF STEP]
using inv_less_0
[PROOF STATE]
proof (prove)
using this:
inverse a < (0::'a)

goal (1 subgoal):
 1. inverse (inverse a) < (0::'a)
[PROOF STEP]
by (rule negative_imp_inverse_negative)
[PROOF STATE]
proof (state)
this:
inverse (inverse a) < (0::'a)

goal (1 subgoal):
 1. a < (0::'a)
[PROOF STEP]
thus "a < 0"
[PROOF STATE]
proof (prove)
using this:
inverse (inverse a) < (0::'a)

goal (1 subgoal):
 1. a < (0::'a)
[PROOF STEP]
using nz
[PROOF STATE]
proof (prove)
using this:
inverse (inverse a) < (0::'a)
a \<noteq> (0::'a)

goal (1 subgoal):
 1. a < (0::'a)
[PROOF STEP]
by (simp add: nonzero_inverse_inverse_eq)
[PROOF STATE]
proof (state)
this:
a < (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linordered_field_no_lb:
  "\<forall>x. \<exists>y. y < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<exists>y. y < x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<exists>y. y < x
[PROOF STEP]
fix x::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<exists>y. y < x
[PROOF STEP]
have m1: "- (1::'a) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (1::'a) < (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- (1::'a) < (0::'a)

goal (1 subgoal):
 1. \<And>x. \<exists>y. y < x
[PROOF STEP]
from add_strict_right_mono[OF m1, where c=x]
[PROOF STATE]
proof (chain)
picking this:
- (1::'a) + x < (0::'a) + x
[PROOF STEP]
have "(- 1) + x < x"
[PROOF STATE]
proof (prove)
using this:
- (1::'a) + x < (0::'a) + x

goal (1 subgoal):
 1. - (1::'a) + x < x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- (1::'a) + x < x

goal (1 subgoal):
 1. \<And>x. \<exists>y. y < x
[PROOF STEP]
thus "\<exists>y. y < x"
[PROOF STATE]
proof (prove)
using this:
- (1::'a) + x < x

goal (1 subgoal):
 1. \<exists>y. y < x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. y < x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linordered_field_no_ub:
  "\<forall>x. \<exists>y. y > x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<exists>y. x < y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<exists>y. x < y
[PROOF STEP]
fix x::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<exists>y. x < y
[PROOF STEP]
have m1: " (1::'a) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) < (1::'a)

goal (1 subgoal):
 1. \<And>x. \<exists>y. x < y
[PROOF STEP]
from add_strict_right_mono[OF m1, where c=x]
[PROOF STATE]
proof (chain)
picking this:
(0::'a) + x < (1::'a) + x
[PROOF STEP]
have "1 + x > x"
[PROOF STATE]
proof (prove)
using this:
(0::'a) + x < (1::'a) + x

goal (1 subgoal):
 1. x < (1::'a) + x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < (1::'a) + x

goal (1 subgoal):
 1. \<And>x. \<exists>y. x < y
[PROOF STEP]
thus "\<exists>y. y > x"
[PROOF STATE]
proof (prove)
using this:
x < (1::'a) + x

goal (1 subgoal):
 1. \<exists>y. x < y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. x < y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_imp_inverse_less:
  assumes less: "a < b" and apos:  "0 < a"
  shows "inverse b < inverse a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse b < inverse a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a < b
(0::'a) < a

goal (1 subgoal):
 1. inverse b < inverse a
[PROOF STEP]
by (metis local.dual_order.strict_iff_order
      local.inverse_inverse_eq local.inverse_le_imp_le local.positive_imp_inverse_positive)


[STATEMENT]
lemma inverse_less_imp_less:
  "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inverse a < inverse b; (0::'a) < a\<rbrakk> \<Longrightarrow> b < a
[PROOF STEP]
using local.inverse_le_imp_le local.order.strict_iff_order
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inverse ?a \<le> inverse ?b; (0::'a) < ?a\<rbrakk> \<Longrightarrow> ?b \<le> ?a
(?a < ?b) = (?a \<le> ?b \<and> ?a \<noteq> ?b)

goal (1 subgoal):
 1. \<lbrakk>inverse a < inverse b; (0::'a) < a\<rbrakk> \<Longrightarrow> b < a
[PROOF STEP]
by blast


[STATEMENT]
lemma inverse_less_iff_less [simp]:
  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; (0::'a) < b\<rbrakk> \<Longrightarrow> (inverse a < inverse b) = (b < a)
[PROOF STEP]
by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)


[STATEMENT]
lemma le_imp_inverse_le:
  "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; (0::'a) < a\<rbrakk> \<Longrightarrow> inverse b \<le> inverse a
[PROOF STEP]
by (force simp add: le_less less_imp_inverse_less)


[STATEMENT]
lemma inverse_le_iff_le [simp]:
  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; (0::'a) < b\<rbrakk> \<Longrightarrow> (inverse a \<le> inverse b) = (b \<le> a)
[PROOF STEP]
by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)


[STATEMENT]
lemma inverse_le_imp_le_neg:
  "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inverse a \<le> inverse b; b < (0::'a)\<rbrakk> \<Longrightarrow> b \<le> a
[PROOF STEP]
by (metis local.inverse_le_imp_le local.inverse_minus_eq local.neg_0_less_iff_less
      local.neg_le_iff_le)


[STATEMENT]
lemma inverse_less_imp_less_neg:
  "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inverse a < inverse b; b < (0::'a)\<rbrakk> \<Longrightarrow> b < a
[PROOF STEP]
using local.dual_order.strict_iff_order local.inverse_le_imp_le_neg
[PROOF STATE]
proof (prove)
using this:
(?b < ?a) = (?b \<le> ?a \<and> ?a \<noteq> ?b)
\<lbrakk>inverse ?a \<le> inverse ?b; ?b < (0::'a)\<rbrakk> \<Longrightarrow> ?b \<le> ?a

goal (1 subgoal):
 1. \<lbrakk>inverse a < inverse b; b < (0::'a)\<rbrakk> \<Longrightarrow> b < a
[PROOF STEP]
by blast


[STATEMENT]
lemma inverse_less_iff_less_neg [simp]:
  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < (0::'a); b < (0::'a)\<rbrakk> \<Longrightarrow> (inverse a < inverse b) = (b < a)
[PROOF STEP]
by (metis local.antisym_conv2 local.inverse_less_imp_less_neg local.negative_imp_inverse_negative
      local.nonzero_inverse_inverse_eq local.order.strict_implies_order)


[STATEMENT]
lemma le_imp_inverse_le_neg:
  "a \<le> b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b \<le> inverse a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; b < (0::'a)\<rbrakk> \<Longrightarrow> inverse b \<le> inverse a
[PROOF STEP]
by (force simp add: le_less less_imp_inverse_less_neg)


[STATEMENT]
lemma inverse_le_iff_le_neg [simp]:
  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < (0::'a); b < (0::'a)\<rbrakk> \<Longrightarrow> (inverse a \<le> inverse b) = (b \<le> a)
[PROOF STEP]
by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)


[STATEMENT]
lemma one_le_inverse:
  "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> (1::'a) \<le> inverse a
[PROOF STEP]
using le_imp_inverse_le [of a 1, unfolded inverse_1]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> (1::'a); (0::'a) < a\<rbrakk> \<Longrightarrow> (1::'a) \<le> inverse a

goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; a \<le> (1::'a)\<rbrakk> \<Longrightarrow> (1::'a) \<le> inverse a
[PROOF STEP]
.


[STATEMENT]
lemma pos_le_divide_eq [field_simps]:
  assumes "0 < c"
  shows "a \<le> b / c \<longleftrightarrow> a * c \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b / c) = (a * c \<le> b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(0::'a) < c

goal (1 subgoal):
 1. (a \<le> b / c) = (a * c \<le> b)
[PROOF STEP]
by (metis local.divide_eq_imp local.divide_inverse_commute
      local.dual_order.order_iff_strict local.dual_order.strict_iff_order
      local.mult_right_mono local.mult_strict_left_mono local.nonzero_divide_eq_eq
      local.order.strict_implies_order local.positive_imp_inverse_positive)


[STATEMENT]
lemma pos_less_divide_eq [field_simps]:
  assumes "0 < c"
  shows "a < b / c \<longleftrightarrow> a * c < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < b / c) = (a * c < b)
[PROOF STEP]
using assms local.dual_order.strict_iff_order local.nonzero_divide_eq_eq local.pos_le_divide_eq
[PROOF STATE]
proof (prove)
using this:
(0::'a) < c
(?b < ?a) = (?b \<le> ?a \<and> ?a \<noteq> ?b)
?c \<noteq> (0::'a) \<Longrightarrow> (?b / ?c = ?a) = (?b = ?a * ?c)
(0::'a) < ?c \<Longrightarrow> (?a \<le> ?b / ?c) = (?a * ?c \<le> ?b)

goal (1 subgoal):
 1. (a < b / c) = (a * c < b)
[PROOF STEP]
by auto


[STATEMENT]
lemma neg_less_divide_eq [field_simps]:
  assumes "c < 0"
  shows "a < b / c \<longleftrightarrow> b < a * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < b / c) = (b < a * c)
[PROOF STEP]
by (metis assms local.minus_divide_divide local.mult_minus_right local.neg_0_less_iff_less
      local.neg_less_iff_less local.pos_less_divide_eq)


[STATEMENT]
lemma neg_le_divide_eq [field_simps]:
  assumes "c < 0"
  shows "a \<le> b / c \<longleftrightarrow> b \<le> a * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b / c) = (b \<le> a * c)
[PROOF STEP]
by (metis assms local.dual_order.order_iff_strict local.dual_order.strict_iff_order
      local.neg_less_divide_eq local.nonzero_divide_eq_eq)


[STATEMENT]
lemma pos_divide_le_eq [field_simps]:
  assumes "0 < c"
  shows "b / c \<le> a \<longleftrightarrow> b \<le> a * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b / c \<le> a) = (b \<le> a * c)
[PROOF STEP]
by (metis assms local.dual_order.strict_iff_order local.nonzero_eq_divide_eq
      local.pos_le_divide_eq)


[STATEMENT]
lemma pos_divide_less_eq [field_simps]:
  assumes "0 < c"
  shows "b / c < a \<longleftrightarrow> b < a * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b / c < a) = (b < a * c)
[PROOF STEP]
by (metis assms local.minus_divide_left local.mult_minus_left local.neg_less_iff_less
      local.pos_less_divide_eq)


[STATEMENT]
lemma neg_divide_le_eq [field_simps]:
  assumes "c < 0"
  shows "b / c \<le> a \<longleftrightarrow> a * c \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b / c \<le> a) = (a * c \<le> b)
[PROOF STEP]
by (metis assms local.minus_divide_left local.mult_minus_left local.neg_le_divide_eq
      local.neg_le_iff_le)


[STATEMENT]
lemma neg_divide_less_eq [field_simps]:
  assumes "c < 0"
  shows "b / c < a \<longleftrightarrow> a * c < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b / c < a) = (a * c < b)
[PROOF STEP]
using assms local.dual_order.strict_iff_order local.neg_divide_le_eq
[PROOF STATE]
proof (prove)
using this:
c < (0::'a)
(?b < ?a) = (?b \<le> ?a \<and> ?a \<noteq> ?b)
?c < (0::'a) \<Longrightarrow> (?b / ?c \<le> ?a) = (?a * ?c \<le> ?b)

goal (1 subgoal):
 1. (b / c < a) = (a * c < b)
[PROOF STEP]
by auto


[STATEMENT]
lemma pos_le_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> a * c \<le> - b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c \<Longrightarrow> (a \<le> - (b / c)) = (a * c \<le> - b)
[PROOF STEP]
unfolding minus_divide_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c \<Longrightarrow> (a \<le> - b / c) = (a * c \<le> - b)
[PROOF STEP]
by (rule pos_le_divide_eq)


[STATEMENT]
lemma neg_le_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> - b \<le> a * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < (0::'a) \<Longrightarrow> (a \<le> - (b / c)) = (- b \<le> a * c)
[PROOF STEP]
unfolding minus_divide_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < (0::'a) \<Longrightarrow> (a \<le> - b / c) = (- b \<le> a * c)
[PROOF STEP]
by (rule neg_le_divide_eq)


[STATEMENT]
lemma pos_less_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < - (b / c) \<longleftrightarrow> a * c < - b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c \<Longrightarrow> (a < - (b / c)) = (a * c < - b)
[PROOF STEP]
unfolding minus_divide_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c \<Longrightarrow> (a < - b / c) = (a * c < - b)
[PROOF STEP]
by (rule pos_less_divide_eq)


[STATEMENT]
lemma neg_less_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < - (b / c) \<longleftrightarrow> - b < a * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < (0::'a) \<Longrightarrow> (a < - (b / c)) = (- b < a * c)
[PROOF STEP]
unfolding minus_divide_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < (0::'a) \<Longrightarrow> (a < - b / c) = (- b < a * c)
[PROOF STEP]
by (rule neg_less_divide_eq)


[STATEMENT]
lemma pos_minus_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) < a \<longleftrightarrow> - b < a * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c \<Longrightarrow> (- (b / c) < a) = (- b < a * c)
[PROOF STEP]
unfolding minus_divide_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c \<Longrightarrow> (- b / c < a) = (- b < a * c)
[PROOF STEP]
by (rule pos_divide_less_eq)


[STATEMENT]
lemma neg_minus_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) < a \<longleftrightarrow> a * c < - b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < (0::'a) \<Longrightarrow> (- (b / c) < a) = (a * c < - b)
[PROOF STEP]
unfolding minus_divide_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < (0::'a) \<Longrightarrow> (- b / c < a) = (a * c < - b)
[PROOF STEP]
by (rule neg_divide_less_eq)


[STATEMENT]
lemma pos_minus_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> - b \<le> a * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c \<Longrightarrow> (- (b / c) \<le> a) = (- b \<le> a * c)
[PROOF STEP]
unfolding minus_divide_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c \<Longrightarrow> (- b / c \<le> a) = (- b \<le> a * c)
[PROOF STEP]
by (rule pos_divide_le_eq)


[STATEMENT]
lemma neg_minus_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> a * c \<le> - b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < (0::'a) \<Longrightarrow> (- (b / c) \<le> a) = (a * c \<le> - b)
[PROOF STEP]
unfolding minus_divide_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < (0::'a) \<Longrightarrow> (- b / c \<le> a) = (a * c \<le> - b)
[PROOF STEP]
by (rule neg_divide_le_eq)


[STATEMENT]
lemma frac_less_eq:
  "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z - w * y) / (y * z) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> (0::'a); z \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (x / y < w / z) = ((x * z - w * y) / (y * z) < (0::'a))
[PROOF STEP]
by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )


[STATEMENT]
lemma frac_le_eq:
  "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> (0::'a); z \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (x / y \<le> w / z) = ((x * z - w * y) / (y * z) \<le> (0::'a))
[PROOF STEP]
by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )


[STATEMENT]
lemma divide_pos_pos[simp]:
  "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> 0 < x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < x; (0::'a) < y\<rbrakk> \<Longrightarrow> (0::'a) < x / y
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma divide_nonneg_pos:
  "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 0 \<le> x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; (0::'a) < y\<rbrakk> \<Longrightarrow> (0::'a) \<le> x / y
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma divide_neg_pos:
  "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> x / y < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < (0::'a); (0::'a) < y\<rbrakk> \<Longrightarrow> x / y < (0::'a)
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma divide_nonpos_pos:
  "x \<le> 0 \<Longrightarrow> 0 < y \<Longrightarrow> x / y \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> (0::'a); (0::'a) < y\<rbrakk> \<Longrightarrow> x / y \<le> (0::'a)
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma divide_pos_neg:
  "0 < x \<Longrightarrow> y < 0 \<Longrightarrow> x / y < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < x; y < (0::'a)\<rbrakk> \<Longrightarrow> x / y < (0::'a)
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma divide_nonneg_neg:
  "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> x / y \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; y < (0::'a)\<rbrakk> \<Longrightarrow> x / y \<le> (0::'a)
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma divide_neg_neg:
  "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> 0 < x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < (0::'a); y < (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) < x / y
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma divide_nonpos_neg:
  "x \<le> 0 \<Longrightarrow> y < 0 \<Longrightarrow> 0 \<le> x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> (0::'a); y < (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) \<le> x / y
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma divide_strict_right_mono:
  "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a / c < b / c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; (0::'a) < c\<rbrakk> \<Longrightarrow> a / c < b / c
[PROOF STEP]
by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
      positive_imp_inverse_positive)


[STATEMENT]
lemma divide_strict_right_mono_neg:
  "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a / c < b / c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < a; c < (0::'a)\<rbrakk> \<Longrightarrow> a / c < b / c
[PROOF STEP]
by (simp add: local.neg_less_divide_eq)


[STATEMENT]
lemma divide_strict_left_mono:
  "b < a \<Longrightarrow> 0 < c \<Longrightarrow> 0 < a*b \<Longrightarrow> c / a < c / b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < a; (0::'a) < c; (0::'a) < a * b\<rbrakk> \<Longrightarrow> c / a < c / b
[PROOF STEP]
by (metis local.divide_neg_pos local.dual_order.strict_iff_order local.frac_less_eq local.less_iff_diff_less_0 local.mult_not_zero local.mult_strict_left_mono)


[STATEMENT]
lemma divide_left_mono:
  "b \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> 0 < a*b \<Longrightarrow> c / a \<le> c / b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; (0::'a) \<le> c; (0::'a) < a * b\<rbrakk> \<Longrightarrow> c / a \<le> c / b
[PROOF STEP]
using local.divide_cancel_left local.divide_strict_left_mono local.dual_order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
(?c / ?a = ?c / ?b) = (?c = (0::'a) \<or> ?a = ?b)
\<lbrakk>?b < ?a; (0::'a) < ?c; (0::'a) < ?a * ?b\<rbrakk> \<Longrightarrow> ?c / ?a < ?c / ?b
(?b \<le> ?a) = (?b < ?a \<or> ?a = ?b)

goal (1 subgoal):
 1. \<lbrakk>b \<le> a; (0::'a) \<le> c; (0::'a) < a * b\<rbrakk> \<Longrightarrow> c / a \<le> c / b
[PROOF STEP]
by auto


[STATEMENT]
lemma divide_strict_left_mono_neg:
  "a < b \<Longrightarrow> c < 0 \<Longrightarrow> 0 < a*b \<Longrightarrow> c / a < c / b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; c < (0::'a); (0::'a) < a * b\<rbrakk> \<Longrightarrow> c / a < c / b
[PROOF STEP]
by (metis local.divide_strict_left_mono local.minus_divide_left local.neg_0_less_iff_less local.neg_less_iff_less mult_commute)


[STATEMENT]
lemma mult_imp_div_pos_le: "0 < y \<Longrightarrow> x \<le> z * y \<Longrightarrow> x / y \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < y; x \<le> z * y\<rbrakk> \<Longrightarrow> x / y \<le> z
[PROOF STEP]
by (subst pos_divide_le_eq, assumption+)


[STATEMENT]
lemma mult_imp_le_div_pos: "0 < y \<Longrightarrow> z * y \<le> x \<Longrightarrow> z \<le> x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < y; z * y \<le> x\<rbrakk> \<Longrightarrow> z \<le> x / y
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma mult_imp_div_pos_less: "0 < y \<Longrightarrow> x < z * y \<Longrightarrow> x / y < z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < y; x < z * y\<rbrakk> \<Longrightarrow> x / y < z
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma mult_imp_less_div_pos: "0 < y \<Longrightarrow> z * y < x \<Longrightarrow> z < x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < y; z * y < x\<rbrakk> \<Longrightarrow> z < x / y
[PROOF STEP]
by(simp add:field_simps)


[STATEMENT]
lemma frac_le: "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> 0 < w \<Longrightarrow> w \<le> z  \<Longrightarrow> x / z \<le> y / w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x \<le> y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z \<le> y / w
[PROOF STEP]
using local.mult_imp_div_pos_le local.mult_imp_le_div_pos local.mult_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) < ?y; ?x \<le> ?z * ?y\<rbrakk> \<Longrightarrow> ?x / ?y \<le> ?z
\<lbrakk>(0::'a) < ?y; ?z * ?y \<le> ?x\<rbrakk> \<Longrightarrow> ?z \<le> ?x / ?y
\<lbrakk>?a \<le> ?b; ?c \<le> ?d; (0::'a) \<le> ?b; (0::'a) \<le> ?c\<rbrakk> \<Longrightarrow> ?a * ?c \<le> ?b * ?d

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x \<le> y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z \<le> y / w
[PROOF STEP]
by auto


[STATEMENT]
lemma frac_less: "0 \<le> x \<Longrightarrow> x < y \<Longrightarrow> 0 < w \<Longrightarrow> w \<le> z \<Longrightarrow> x / z < y / w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
assume a1: "w \<le> z"
[PROOF STATE]
proof (state)
this:
w \<le> z

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
assume a2: "0 < w"
[PROOF STATE]
proof (state)
this:
(0::'a) < w

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
assume a3: "0 \<le> x"
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> x

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
assume a4: "x < y"
[PROOF STATE]
proof (state)
this:
x < y

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
have f5: "a = 0 \<or> (b = c / a) = (b * a = c)"
    for a b c::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = (0::'a) \<or> (b = c / a) = (b * a = c)
[PROOF STEP]
by (meson local.nonzero_eq_divide_eq)
[PROOF STATE]
proof (state)
this:
?a1 = (0::'a) \<or> (?b1 = ?c1 / ?a1) = (?b1 * ?a1 = ?c1)

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
have f6: "0 < z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < z
[PROOF STEP]
using a2 a1 less_le_trans
[PROOF STATE]
proof (prove)
using this:
(0::'a) < w
w \<le> z
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. (0::'a) < z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(0::'a) < z

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
have "z \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<noteq> (0::'a)
[PROOF STEP]
using a2 a1
[PROOF STATE]
proof (prove)
using this:
(0::'a) < w
w \<le> z

goal (1 subgoal):
 1. z \<noteq> (0::'a)
[PROOF STEP]
by (meson local.leD)
[PROOF STATE]
proof (state)
this:
z \<noteq> (0::'a)

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z \<noteq> (0::'a)

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
have "x / z \<noteq> y / w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x / z \<noteq> y / w
[PROOF STEP]
using a1 a2 a3 a4 local.frac_eq_eq local.mult_less_le_imp_less
[PROOF STATE]
proof (prove)
using this:
w \<le> z
(0::'a) < w
(0::'a) \<le> x
x < y
\<lbrakk>?y \<noteq> (0::'a); ?z \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (?x / ?y = ?w / ?z) = (?x * ?z = ?w * ?y)
\<lbrakk>?a < ?b; ?c \<le> ?d; (0::'a) \<le> ?a; (0::'a) < ?c\<rbrakk> \<Longrightarrow> ?a * ?c < ?b * ?d

goal (1 subgoal):
 1. x / z \<noteq> y / w
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x / z \<noteq> y / w

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> (0::'a)
x / z \<noteq> y / w
[PROOF STEP]
have "x / z \<noteq> y / w"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0::'a)
x / z \<noteq> y / w

goal (1 subgoal):
 1. x / z \<noteq> y / w
[PROOF STEP]
using f5
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0::'a)
x / z \<noteq> y / w
?a1 = (0::'a) \<or> (?b1 = ?c1 / ?a1) = (?b1 * ?a1 = ?c1)

goal (1 subgoal):
 1. x / z \<noteq> y / w
[PROOF STEP]
by (metis (no_types))
[PROOF STATE]
proof (state)
this:
x / z \<noteq> y / w

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x < y; (0::'a) < w; w \<le> z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x / z \<noteq> y / w

goal (1 subgoal):
 1. x / z < y / w
[PROOF STEP]
using a4 a3 a2 a1
[PROOF STATE]
proof (prove)
using this:
x / z \<noteq> y / w
x < y
(0::'a) \<le> x
(0::'a) < w
w \<le> z

goal (1 subgoal):
 1. x / z < y / w
[PROOF STEP]
by (meson local.frac_le local.order.not_eq_order_implies_strict
        local.order.strict_implies_order)
[PROOF STATE]
proof (state)
this:
x / z < y / w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frac_less2: "0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> 0 < w \<Longrightarrow> w < z  \<Longrightarrow> x / z < y / w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < x; x \<le> y; (0::'a) < w; w < z\<rbrakk> \<Longrightarrow> x / z < y / w
[PROOF STEP]
by (metis local.antisym_conv2 local.divide_cancel_left local.dual_order.strict_implies_order
      local.frac_le local.frac_less)


[STATEMENT]
lemma less_half_sum: "a < b \<Longrightarrow> a < (a+b) / (1+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < b \<Longrightarrow> a < (a + b) / ((1::'a) + (1::'a))
[PROOF STEP]
by (metis local.add_pos_pos local.add_strict_left_mono local.mult_imp_less_div_pos local.semiring_normalization_rules(4) local.zero_less_one mult_commute)


[STATEMENT]
lemma gt_half_sum: "a < b \<Longrightarrow> (a+b)/(1+1) < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < b \<Longrightarrow> (a + b) / ((1::'a) + (1::'a)) < b
[PROOF STEP]
by (metis local.add_pos_pos local.add_strict_left_mono local.mult_imp_div_pos_less local.semiring_normalization_rules(24) local.semiring_normalization_rules(4) local.zero_less_one mult_commute)


[STATEMENT]
lemma dense_le_bounded:
  fixes x y z :: 'a
  assumes "x < y"
    and *: "\<And>w. \<lbrakk> x < w ; w < y \<rbrakk> \<Longrightarrow> w \<le> z"
  shows "y \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> z
[PROOF STEP]
proof (rule dense_le)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x < y \<Longrightarrow> x \<le> z
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x < y \<Longrightarrow> x \<le> z
[PROOF STEP]
assume "w < y"
[PROOF STATE]
proof (state)
this:
w < y

goal (1 subgoal):
 1. \<And>x. x < y \<Longrightarrow> x \<le> z
[PROOF STEP]
from dense[OF \<open>x < y\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>z>x. z < y
[PROOF STEP]
obtain u where "x < u" "u < y"
[PROOF STATE]
proof (prove)
using this:
\<exists>z>x. z < y

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>x < u; u < y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by safe
[PROOF STATE]
proof (state)
this:
x < u
u < y

goal (1 subgoal):
 1. \<And>x. x < y \<Longrightarrow> x \<le> z
[PROOF STEP]
have "u \<le> w \<or> w \<le> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> w \<or> w \<le> u
[PROOF STEP]
using \<open>u < y\<close> \<open>w < y\<close> comparable local.order.strict_implies_order
[PROOF STATE]
proof (prove)
using this:
u < y
w < y
\<lbrakk>?a \<le> ?c \<or> ?c \<le> ?a; ?b \<le> ?c \<or> ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
?a < ?b \<Longrightarrow> ?a \<le> ?b

goal (1 subgoal):
 1. u \<le> w \<or> w \<le> u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<le> w \<or> w \<le> u

goal (1 subgoal):
 1. \<And>x. x < y \<Longrightarrow> x \<le> z
[PROOF STEP]
thus "w \<le> z"
[PROOF STATE]
proof (prove)
using this:
u \<le> w \<or> w \<le> u

goal (1 subgoal):
 1. w \<le> z
[PROOF STEP]
using "*" \<open>u < y\<close> \<open>w < y\<close> \<open>x < u\<close> local.dual_order.trans local.order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
u \<le> w \<or> w \<le> u
\<lbrakk>x < ?w1; ?w1 < y\<rbrakk> \<Longrightarrow> ?w1 \<le> z
u < y
w < y
x < u
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

goal (1 subgoal):
 1. w \<le> z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<le> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonzero_abs_inverse:
  "a \<noteq> 0 \<Longrightarrow> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>
[PROOF STEP]
by (rule abs_inverse)


[STATEMENT]
lemma nonzero_abs_divide:
  "b \<noteq> 0 \<Longrightarrow> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<noteq> (0::'a) \<Longrightarrow> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>
[PROOF STEP]
by (rule abs_divide)


[STATEMENT]
lemma field_le_epsilon:
  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
  shows "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
proof (rule dense_le)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa < x \<Longrightarrow> xa \<le> y
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa < x \<Longrightarrow> xa \<le> y
[PROOF STEP]
assume "t < x"
[PROOF STATE]
proof (state)
this:
t < x

goal (1 subgoal):
 1. \<And>xa. xa < x \<Longrightarrow> xa \<le> y
[PROOF STEP]
hence "0 < x - t"
[PROOF STATE]
proof (prove)
using this:
t < x

goal (1 subgoal):
 1. (0::'a) < x - t
[PROOF STEP]
by (simp add: less_diff_eq)
[PROOF STATE]
proof (state)
this:
(0::'a) < x - t

goal (1 subgoal):
 1. \<And>xa. xa < x \<Longrightarrow> xa \<le> y
[PROOF STEP]
from e [OF this]
[PROOF STATE]
proof (chain)
picking this:
x \<le> y + (x - t)
[PROOF STEP]
have "x + 0 \<le> x + (y - t)"
[PROOF STATE]
proof (prove)
using this:
x \<le> y + (x - t)

goal (1 subgoal):
 1. x + (0::'a) \<le> x + (y - t)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
x + (0::'a) \<le> x + (y - t)

goal (1 subgoal):
 1. \<And>xa. xa < x \<Longrightarrow> xa \<le> y
[PROOF STEP]
hence "0 \<le> y - t"
[PROOF STATE]
proof (prove)
using this:
x + (0::'a) \<le> x + (y - t)

goal (1 subgoal):
 1. (0::'a) \<le> y - t
[PROOF STEP]
by (simp only: add_le_cancel_left)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> y - t

goal (1 subgoal):
 1. \<And>xa. xa < x \<Longrightarrow> xa \<le> y
[PROOF STEP]
thus "t \<le> y"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> y - t

goal (1 subgoal):
 1. t \<le> y
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
t \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inverse_positive_iff_positive [simp]:
  "(0 < inverse a) = (0 < a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) < inverse a) = ((0::'a) < a)
[PROOF STEP]
using local.positive_imp_inverse_positive
[PROOF STATE]
proof (prove)
using this:
(0::'a) < ?a \<Longrightarrow> (0::'a) < inverse ?a

goal (1 subgoal):
 1. ((0::'a) < inverse a) = ((0::'a) < a)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma inverse_negative_iff_negative [simp]:
  "(inverse a < 0) = (a < 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse a < (0::'a)) = (a < (0::'a))
[PROOF STEP]
using local.negative_imp_inverse_negative
[PROOF STATE]
proof (prove)
using this:
?a < (0::'a) \<Longrightarrow> inverse ?a < (0::'a)

goal (1 subgoal):
 1. (inverse a < (0::'a)) = (a < (0::'a))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma inverse_nonnegative_iff_nonnegative [simp]:
  "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) \<le> inverse a) = ((0::'a) \<le> a)
[PROOF STEP]
by (simp add: local.dual_order.order_iff_strict)


[STATEMENT]
lemma inverse_nonpositive_iff_nonpositive [simp]:
  "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse a \<le> (0::'a)) = (a \<le> (0::'a))
[PROOF STEP]
using local.inverse_nonnegative_iff_nonnegative local.neg_0_le_iff_le
[PROOF STATE]
proof (prove)
using this:
((0::'a) \<le> inverse ?a) = ((0::'a) \<le> ?a)
((0::'a) \<le> - ?a) = (?a \<le> (0::'a))

goal (1 subgoal):
 1. (inverse a \<le> (0::'a)) = (a \<le> (0::'a))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma one_less_inverse_iff: "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) < inverse x) = ((0::'a) < x \<and> x < (1::'a))
[PROOF STEP]
using less_trans[of 1 x 0 for x]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(1::'a) < ?xa3; ?xa3 < (0::'a)\<rbrakk> \<Longrightarrow> (1::'a) < (0::'a)

goal (1 subgoal):
 1. ((1::'a) < inverse x) = ((0::'a) < x \<and> x < (1::'a))
[PROOF STEP]
by (metis local.dual_order.strict_trans local.inverse_1 local.inverse_less_imp_less local.inverse_positive_iff_positive local.one_less_inverse local.zero_less_one)


[STATEMENT]
lemma one_le_inverse_iff: "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) \<le> inverse x) = ((0::'a) < x \<and> x \<le> (1::'a))
[PROOF STEP]
by (metis local.dual_order.strict_trans1 local.inverse_1 local.inverse_le_imp_le local.inverse_positive_iff_positive local.one_le_inverse local.zero_less_one)


[STATEMENT]
lemma inverse_less_1_iff: "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse x < (1::'a)) = (x \<le> (0::'a) \<or> (1::'a) < x)
[PROOF STEP]
proof (rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inverse x < (1::'a) \<Longrightarrow> x \<le> (0::'a) \<or> (1::'a) < x
 2. x \<le> (0::'a) \<or> (1::'a) < x \<Longrightarrow> inverse x < (1::'a)
[PROOF STEP]
assume invx1: "inverse x < 1"
[PROOF STATE]
proof (state)
this:
inverse x < (1::'a)

goal (2 subgoals):
 1. inverse x < (1::'a) \<Longrightarrow> x \<le> (0::'a) \<or> (1::'a) < x
 2. x \<le> (0::'a) \<or> (1::'a) < x \<Longrightarrow> inverse x < (1::'a)
[PROOF STEP]
have "inverse x \<le> 0 \<or> inverse x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse x \<le> (0::'a) \<or> (0::'a) \<le> inverse x
[PROOF STEP]
using comparable invx1 local.order.strict_implies_order local.zero_less_one
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<le> ?c \<or> ?c \<le> ?a; ?b \<le> ?c \<or> ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?a \<le> ?b \<or> ?b \<le> ?a
inverse x < (1::'a)
?a < ?b \<Longrightarrow> ?a \<le> ?b
(0::'a) < (1::'a)

goal (1 subgoal):
 1. inverse x \<le> (0::'a) \<or> (0::'a) \<le> inverse x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse x \<le> (0::'a) \<or> (0::'a) \<le> inverse x

goal (2 subgoals):
 1. inverse x < (1::'a) \<Longrightarrow> x \<le> (0::'a) \<or> (1::'a) < x
 2. x \<le> (0::'a) \<or> (1::'a) < x \<Longrightarrow> inverse x < (1::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inverse x \<le> (0::'a) \<or> (0::'a) \<le> inverse x
[PROOF STEP]
consider (leq0) "inverse x \<le> 0" | (pos) "inverse x > 0" | (zero) "inverse x = 0"
[PROOF STATE]
proof (prove)
using this:
inverse x \<le> (0::'a) \<or> (0::'a) \<le> inverse x

goal (1 subgoal):
 1. \<lbrakk>inverse x \<le> (0::'a) \<Longrightarrow> thesis; (0::'a) < inverse x \<Longrightarrow> thesis; inverse x = (0::'a) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using local.antisym_conv1
[PROOF STATE]
proof (prove)
using this:
inverse x \<le> (0::'a) \<or> (0::'a) \<le> inverse x
\<not> ?x < ?y \<Longrightarrow> (?x \<le> ?y) = (?x = ?y)

goal (1 subgoal):
 1. \<lbrakk>inverse x \<le> (0::'a) \<Longrightarrow> thesis; (0::'a) < inverse x \<Longrightarrow> thesis; inverse x = (0::'a) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>inverse x \<le> (0::'a) \<Longrightarrow> ?thesis1; (0::'a) < inverse x \<Longrightarrow> ?thesis1; inverse x = (0::'a) \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (2 subgoals):
 1. inverse x < (1::'a) \<Longrightarrow> x \<le> (0::'a) \<or> (1::'a) < x
 2. x \<le> (0::'a) \<or> (1::'a) < x \<Longrightarrow> inverse x < (1::'a)
[PROOF STEP]
thus "x \<le> 0 \<or> 1 < x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inverse x \<le> (0::'a) \<Longrightarrow> ?thesis1; (0::'a) < inverse x \<Longrightarrow> ?thesis1; inverse x = (0::'a) \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. x \<le> (0::'a) \<or> (1::'a) < x
[PROOF STEP]
by (metis invx1 local.eq_refl local.inverse_1 inverse_less_imp_less
              inverse_nonpositive_iff_nonpositive inverse_positive_iff_positive)
[PROOF STATE]
proof (state)
this:
x \<le> (0::'a) \<or> (1::'a) < x

goal (1 subgoal):
 1. x \<le> (0::'a) \<or> (1::'a) < x \<Longrightarrow> inverse x < (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> (0::'a) \<or> (1::'a) < x \<Longrightarrow> inverse x < (1::'a)
[PROOF STEP]
assume "x \<le> 0 \<or> 1 < x"
[PROOF STATE]
proof (state)
this:
x \<le> (0::'a) \<or> (1::'a) < x

goal (1 subgoal):
 1. x \<le> (0::'a) \<or> (1::'a) < x \<Longrightarrow> inverse x < (1::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<le> (0::'a) \<or> (1::'a) < x
[PROOF STEP]
consider (neg) "x \<le> 0" | (g1) "1 < x"
[PROOF STATE]
proof (prove)
using this:
x \<le> (0::'a) \<or> (1::'a) < x

goal (1 subgoal):
 1. \<lbrakk>x \<le> (0::'a) \<Longrightarrow> thesis; (1::'a) < x \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<le> (0::'a) \<Longrightarrow> ?thesis1; (1::'a) < x \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. x \<le> (0::'a) \<or> (1::'a) < x \<Longrightarrow> inverse x < (1::'a)
[PROOF STEP]
thus "inverse x < 1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<le> (0::'a) \<Longrightarrow> ?thesis1; (1::'a) < x \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. inverse x < (1::'a)
[PROOF STEP]
by (metis local.dual_order.not_eq_order_implies_strict local.dual_order.strict_trans
        local.inverse_1 local.inverse_negative_iff_negative local.inverse_zero
        local.less_imp_inverse_less local.zero_less_one)
[PROOF STATE]
proof (state)
this:
inverse x < (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse x \<le> (1::'a)) = (x \<le> (0::'a) \<or> (1::'a) \<le> x)
[PROOF STEP]
by (metis local.dual_order.order_iff_strict local.inverse_1 local.inverse_le_iff_le
      local.inverse_less_1_iff local.one_le_inverse_iff)


[STATEMENT]
lemma zero_le_divide_1_iff [simp]:
  "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) \<le> (1::'a) / a) = ((0::'a) \<le> a)
[PROOF STEP]
using local.dual_order.order_iff_strict local.inverse_eq_divide
    local.inverse_positive_iff_positive
[PROOF STATE]
proof (prove)
using this:
(?b \<le> ?a) = (?b < ?a \<or> ?a = ?b)
inverse ?a = (1::'a) / ?a
((0::'a) < inverse ?a) = ((0::'a) < ?a)

goal (1 subgoal):
 1. ((0::'a) \<le> (1::'a) / a) = ((0::'a) \<le> a)
[PROOF STEP]
by auto


[STATEMENT]
lemma zero_less_divide_1_iff [simp]:
  "0 < 1 / a \<longleftrightarrow> 0 < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) < (1::'a) / a) = ((0::'a) < a)
[PROOF STEP]
by (simp add: local.dual_order.strict_iff_order)


[STATEMENT]
lemma divide_le_0_1_iff [simp]:
  "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) / a \<le> (0::'a)) = (a \<le> (0::'a))
[PROOF STEP]
by (smt local.abs_0 local.abs_1 local.abs_divide local.abs_neg local.abs_nn
      local.divide_cancel_left local.le_minus_iff local.minus_divide_right local.zero_neq_one)


[STATEMENT]
lemma divide_less_0_1_iff [simp]:
  "1 / a < 0 \<longleftrightarrow> a < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) / a < (0::'a)) = (a < (0::'a))
[PROOF STEP]
using local.dual_order.strict_iff_order
[PROOF STATE]
proof (prove)
using this:
(?b < ?a) = (?b \<le> ?a \<and> ?a \<noteq> ?b)

goal (1 subgoal):
 1. ((1::'a) / a < (0::'a)) = (a < (0::'a))
[PROOF STEP]
by auto


[STATEMENT]
lemma divide_right_mono:
  "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a/c \<le> b/c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; (0::'a) \<le> c\<rbrakk> \<Longrightarrow> a / c \<le> b / c
[PROOF STEP]
using local.divide_cancel_right local.divide_strict_right_mono local.dual_order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
(?a / ?c = ?b / ?c) = (?c = (0::'a) \<or> ?a = ?b)
\<lbrakk>?a < ?b; (0::'a) < ?c\<rbrakk> \<Longrightarrow> ?a / ?c < ?b / ?c
(?b \<le> ?a) = (?b < ?a \<or> ?a = ?b)

goal (1 subgoal):
 1. \<lbrakk>a \<le> b; (0::'a) \<le> c\<rbrakk> \<Longrightarrow> a / c \<le> b / c
[PROOF STEP]
by blast


[STATEMENT]
lemma divide_right_mono_neg: "a \<le> b
    \<Longrightarrow> c \<le> 0 \<Longrightarrow> b / c \<le> a / c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; c \<le> (0::'a)\<rbrakk> \<Longrightarrow> b / c \<le> a / c
[PROOF STEP]
by (metis local.divide_cancel_right local.divide_strict_right_mono_neg local.dual_order.strict_implies_order local.eq_refl local.le_imp_less_or_eq)


[STATEMENT]
lemma divide_left_mono_neg: "a \<le> b
    \<Longrightarrow> c \<le> 0 \<Longrightarrow> 0 < a * b \<Longrightarrow> c / a \<le> c / b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; c \<le> (0::'a); (0::'a) < a * b\<rbrakk> \<Longrightarrow> c / a \<le> c / b
[PROOF STEP]
by (metis local.divide_left_mono local.minus_divide_left local.neg_0_le_iff_le local.neg_le_iff_le mult_commute)


[STATEMENT]
lemma divide_nonneg_nonneg [simp]:
  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; (0::'a) \<le> y\<rbrakk> \<Longrightarrow> (0::'a) \<le> x / y
[PROOF STEP]
using local.divide_eq_0_iff local.divide_nonneg_pos local.dual_order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
(?a / ?b = (0::'a)) = (?a = (0::'a) \<or> ?b = (0::'a))
\<lbrakk>(0::'a) \<le> ?x; (0::'a) < ?y\<rbrakk> \<Longrightarrow> (0::'a) \<le> ?x / ?y
(?b \<le> ?a) = (?b < ?a \<or> ?a = ?b)

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; (0::'a) \<le> y\<rbrakk> \<Longrightarrow> (0::'a) \<le> x / y
[PROOF STEP]
by blast


[STATEMENT]
lemma divide_nonpos_nonpos:
  "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> 0 \<le> x / y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> (0::'a); y \<le> (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) \<le> x / y
[PROOF STEP]
using local.divide_nonpos_neg local.dual_order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> (0::'a); ?y < (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) \<le> ?x / ?y
(?b \<le> ?a) = (?b < ?a \<or> ?a = ?b)

goal (1 subgoal):
 1. \<lbrakk>x \<le> (0::'a); y \<le> (0::'a)\<rbrakk> \<Longrightarrow> (0::'a) \<le> x / y
[PROOF STEP]
by auto


[STATEMENT]
lemma divide_nonneg_nonpos:
  "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> x / y \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; y \<le> (0::'a)\<rbrakk> \<Longrightarrow> x / y \<le> (0::'a)
[PROOF STEP]
by (metis local.divide_eq_0_iff local.divide_nonneg_neg local.dual_order.order_iff_strict)


[STATEMENT]
lemma divide_nonpos_nonneg:
  "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x / y \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> (0::'a); (0::'a) \<le> y\<rbrakk> \<Longrightarrow> x / y \<le> (0::'a)
[PROOF STEP]
using local.divide_nonpos_pos local.dual_order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> (0::'a); (0::'a) < ?y\<rbrakk> \<Longrightarrow> ?x / ?y \<le> (0::'a)
(?b \<le> ?a) = (?b < ?a \<or> ?a = ?b)

goal (1 subgoal):
 1. \<lbrakk>x \<le> (0::'a); (0::'a) \<le> y\<rbrakk> \<Longrightarrow> x / y \<le> (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma le_divide_eq_1_pos [simp]:
  "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < a \<Longrightarrow> ((1::'a) \<le> b / a) = (a \<le> b)
[PROOF STEP]
by (simp add: local.pos_le_divide_eq)


[STATEMENT]
lemma divide_le_eq_1_pos [simp]:
  "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < a \<Longrightarrow> (b / a \<le> (1::'a)) = (b \<le> a)
[PROOF STEP]
using local.pos_divide_le_eq
[PROOF STATE]
proof (prove)
using this:
(0::'a) < ?c \<Longrightarrow> (?b / ?c \<le> ?a) = (?b \<le> ?a * ?c)

goal (1 subgoal):
 1. (0::'a) < a \<Longrightarrow> (b / a \<le> (1::'a)) = (b \<le> a)
[PROOF STEP]
by auto


[STATEMENT]
lemma divide_le_eq_1_neg [simp]:
  "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < (0::'a) \<Longrightarrow> (b / a \<le> (1::'a)) = (a \<le> b)
[PROOF STEP]
by (metis local.divide_le_eq_1_pos local.minus_divide_divide local.neg_0_less_iff_less
      local.neg_le_iff_le)


[STATEMENT]
lemma less_divide_eq_1_pos [simp]:
  "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < a \<Longrightarrow> ((1::'a) < b / a) = (a < b)
[PROOF STEP]
by (simp add: local.dual_order.strict_iff_order)


[STATEMENT]
lemma less_divide_eq_1_neg [simp]:
  "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < (0::'a) \<Longrightarrow> ((1::'a) < b / a) = (b < a)
[PROOF STEP]
using local.dual_order.strict_iff_order
[PROOF STATE]
proof (prove)
using this:
(?b < ?a) = (?b \<le> ?a \<and> ?a \<noteq> ?b)

goal (1 subgoal):
 1. a < (0::'a) \<Longrightarrow> ((1::'a) < b / a) = (b < a)
[PROOF STEP]
by auto


[STATEMENT]
lemma divide_less_eq_1_pos [simp]:
  "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < a \<Longrightarrow> (b / a < (1::'a)) = (b < a)
[PROOF STEP]
using local.divide_le_eq_1_pos local.dual_order.strict_iff_order
[PROOF STATE]
proof (prove)
using this:
(0::'a) < ?a \<Longrightarrow> (?b / ?a \<le> (1::'a)) = (?b \<le> ?a)
(?b < ?a) = (?b \<le> ?a \<and> ?a \<noteq> ?b)

goal (1 subgoal):
 1. (0::'a) < a \<Longrightarrow> (b / a < (1::'a)) = (b < a)
[PROOF STEP]
by auto


[STATEMENT]
lemma divide_less_eq_1_neg [simp]:
  "a < 0 \<Longrightarrow> b/a < 1 \<longleftrightarrow> a < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < (0::'a) \<Longrightarrow> (b / a < (1::'a)) = (a < b)
[PROOF STEP]
using local.dual_order.strict_iff_order
[PROOF STATE]
proof (prove)
using this:
(?b < ?a) = (?b \<le> ?a \<and> ?a \<noteq> ?b)

goal (1 subgoal):
 1. a < (0::'a) \<Longrightarrow> (b / a < (1::'a)) = (a < b)
[PROOF STEP]
by auto


[STATEMENT]
lemma abs_div_pos: "0 < y \<Longrightarrow>
    \<bar>x\<bar> / y = \<bar>x / y\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < y \<Longrightarrow> \<bar>x\<bar> / y = \<bar>x / y\<bar>
[PROOF STEP]
by (simp add: local.abs_pos)


[STATEMENT]
lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / \<bar>b\<bar>) = (0 \<le> a | b = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) \<le> a / \<bar>b\<bar>) = ((0::'a) \<le> a \<or> b = (0::'a))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (0::'a) \<le> a / \<bar>b\<bar> \<Longrightarrow> (0::'a) \<le> a \<or> b = (0::'a)
 2. (0::'a) \<le> a \<or> b = (0::'a) \<Longrightarrow> (0::'a) \<le> a / \<bar>b\<bar>
[PROOF STEP]
assume assm: "0 \<le> a / \<bar>b\<bar>"
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a / \<bar>b\<bar>

goal (2 subgoals):
 1. (0::'a) \<le> a / \<bar>b\<bar> \<Longrightarrow> (0::'a) \<le> a \<or> b = (0::'a)
 2. (0::'a) \<le> a \<or> b = (0::'a) \<Longrightarrow> (0::'a) \<le> a / \<bar>b\<bar>
[PROOF STEP]
have absb: "abs b \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> \<bar>b\<bar>
[PROOF STEP]
by (fact abs_nn)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> \<bar>b\<bar>

goal (2 subgoals):
 1. (0::'a) \<le> a / \<bar>b\<bar> \<Longrightarrow> (0::'a) \<le> a \<or> b = (0::'a)
 2. (0::'a) \<le> a \<or> b = (0::'a) \<Longrightarrow> (0::'a) \<le> a / \<bar>b\<bar>
[PROOF STEP]
thus "0 \<le> a \<or> b = 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> \<bar>b\<bar>

goal (1 subgoal):
 1. (0::'a) \<le> a \<or> b = (0::'a)
[PROOF STEP]
using absb assm local.abs_eq_0_iff local.mult_nonneg_nonneg
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> \<bar>b\<bar>
(0::'a) \<le> \<bar>b\<bar>
(0::'a) \<le> a / \<bar>b\<bar>
(\<bar>?a\<bar> = (0::'a)) = (?a = (0::'a))
\<lbrakk>(0::'a) \<le> ?a; (0::'a) \<le> ?b\<rbrakk> \<Longrightarrow> (0::'a) \<le> ?a * ?b

goal (1 subgoal):
 1. (0::'a) \<le> a \<or> b = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a \<or> b = (0::'a)

goal (1 subgoal):
 1. (0::'a) \<le> a \<or> b = (0::'a) \<Longrightarrow> (0::'a) \<le> a / \<bar>b\<bar>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) \<le> a \<or> b = (0::'a) \<Longrightarrow> (0::'a) \<le> a / \<bar>b\<bar>
[PROOF STEP]
assume "0 \<le> a \<or> b = 0"
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a \<or> b = (0::'a)

goal (1 subgoal):
 1. (0::'a) \<le> a \<or> b = (0::'a) \<Longrightarrow> (0::'a) \<le> a / \<bar>b\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> a \<or> b = (0::'a)
[PROOF STEP]
consider (a) "0 \<le> a" | (b) "b = 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a \<or> b = (0::'a)

goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> a \<Longrightarrow> thesis; b = (0::'a) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>(0::'a) \<le> a \<Longrightarrow> ?thesis1; b = (0::'a) \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. (0::'a) \<le> a \<or> b = (0::'a) \<Longrightarrow> (0::'a) \<le> a / \<bar>b\<bar>
[PROOF STEP]
thus "0 \<le> a / \<bar>b\<bar>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) \<le> a \<Longrightarrow> ?thesis1; b = (0::'a) \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. (0::'a) \<le> a / \<bar>b\<bar>
[PROOF STEP]
by (metis local.abs_eq_0_iff local.abs_nn local.divide_eq_0_iff local.divide_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a / \<bar>b\<bar>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 | b = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a / \<bar>b\<bar> \<le> (0::'a)) = (a \<le> (0::'a) \<or> b = (0::'a))
[PROOF STEP]
by (metis local.minus_divide_left local.neg_0_le_iff_le local.zero_le_divide_abs_iff)


[STATEMENT]
lemma scaling_mono:
  assumes "u \<le> v" and "0 \<le> r" and "r \<le> s"
  shows "u + r * (v - u) / s \<le> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u + r * (v - u) / s \<le> v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u + r * (v - u) / s \<le> v
[PROOF STEP]
have "r/s \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r / s \<le> (1::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<le> v
(0::'a) \<le> r
r \<le> s

goal (1 subgoal):
 1. r / s \<le> (1::'a)
[PROOF STEP]
by (metis local.divide_le_eq_1_pos local.division_ring_divide_zero
        local.dual_order.order_iff_strict local.dual_order.trans local.zero_less_one)
[PROOF STATE]
proof (state)
this:
r / s \<le> (1::'a)

goal (1 subgoal):
 1. u + r * (v - u) / s \<le> v
[PROOF STEP]
hence "(r/s) * (v - u) \<le> 1 * (v - u)"
[PROOF STATE]
proof (prove)
using this:
r / s \<le> (1::'a)

goal (1 subgoal):
 1. r / s * (v - u) \<le> (1::'a) * (v - u)
[PROOF STEP]
using assms(1) local.diff_ge_0_iff_ge local.mult_right_mono
[PROOF STATE]
proof (prove)
using this:
r / s \<le> (1::'a)
u \<le> v
((0::'a) \<le> ?a - ?b) = (?b \<le> ?a)
\<lbrakk>?a \<le> ?b; (0::'a) \<le> ?c\<rbrakk> \<Longrightarrow> ?a * ?c \<le> ?b * ?c

goal (1 subgoal):
 1. r / s * (v - u) \<le> (1::'a) * (v - u)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r / s * (v - u) \<le> (1::'a) * (v - u)

goal (1 subgoal):
 1. u + r * (v - u) / s \<le> v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r / s * (v - u) \<le> (1::'a) * (v - u)

goal (1 subgoal):
 1. u + r * (v - u) / s \<le> v
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
u + r * (v - u) / s \<le> v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_eq_complexI: "Re x \<le> Re y \<Longrightarrow> Im x = Im y \<Longrightarrow> x\<le>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re x \<le> Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x \<le> y
[PROOF STEP]
unfolding less_eq_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re x \<le> Re y; Im x = Im y\<rbrakk> \<Longrightarrow> Re x \<le> Re y \<and> Im x = Im y
[PROOF STEP]
by simp


[STATEMENT]
lemma less_complexI: "Re x < Re y \<Longrightarrow> Im x = Im y \<Longrightarrow> x<y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re x < Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x < y
[PROOF STEP]
unfolding less_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re x < Re y; Im x = Im y\<rbrakk> \<Longrightarrow> Re x < Re y \<and> Im x = Im y
[PROOF STEP]
by simp


[STATEMENT]
lemma complex_of_real_mono:
  "x \<le> y \<Longrightarrow> complex_of_real x \<le> complex_of_real y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> complex_of_real x \<le> complex_of_real y
[PROOF STEP]
unfolding less_eq_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> Re (complex_of_real x) \<le> Re (complex_of_real y) \<and> Im (complex_of_real x) = Im (complex_of_real y)
[PROOF STEP]
by auto


[STATEMENT]
lemma complex_of_real_mono_iff[simp]:
  "complex_of_real x \<le> complex_of_real y \<longleftrightarrow> x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complex_of_real x \<le> complex_of_real y) = (x \<le> y)
[PROOF STEP]
unfolding less_eq_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re (complex_of_real x) \<le> Re (complex_of_real y) \<and> Im (complex_of_real x) = Im (complex_of_real y)) = (x \<le> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma complex_of_real_strict_mono_iff[simp]:
  "complex_of_real x < complex_of_real y \<longleftrightarrow> x < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complex_of_real x < complex_of_real y) = (x < y)
[PROOF STEP]
unfolding less_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re (complex_of_real x) < Re (complex_of_real y) \<and> Im (complex_of_real x) = Im (complex_of_real y)) = (x < y)
[PROOF STEP]
by auto


[STATEMENT]
lemma complex_of_real_nn_iff[simp]:
  "0 \<le> complex_of_real y \<longleftrightarrow> 0 \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> complex_of_real y) = (0 \<le> y)
[PROOF STEP]
unfolding less_eq_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re 0 \<le> Re (complex_of_real y) \<and> Im 0 = Im (complex_of_real y)) = (0 \<le> y)
[PROOF STEP]
by auto


[STATEMENT]
lemma complex_of_real_pos_iff[simp]:
  "0 < complex_of_real y \<longleftrightarrow> 0 < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < complex_of_real y) = (0 < y)
[PROOF STEP]
unfolding less_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re 0 < Re (complex_of_real y) \<and> Im 0 = Im (complex_of_real y)) = (0 < y)
[PROOF STEP]
by auto


[STATEMENT]
lemma Re_mono: "x \<le> y \<Longrightarrow> Re x \<le> Re y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> Re x \<le> Re y
[PROOF STEP]
unfolding less_eq_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re x \<le> Re y \<and> Im x = Im y \<Longrightarrow> Re x \<le> Re y
[PROOF STEP]
by simp


[STATEMENT]
lemma comp_Im_same: "x \<le> y \<Longrightarrow> Im x = Im y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> Im x = Im y
[PROOF STEP]
unfolding less_eq_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re x \<le> Re y \<and> Im x = Im y \<Longrightarrow> Im x = Im y
[PROOF STEP]
by simp


[STATEMENT]
lemma Re_strict_mono: "x < y \<Longrightarrow> Re x < Re y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> Re x < Re y
[PROOF STEP]
unfolding less_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re x < Re y \<and> Im x = Im y \<Longrightarrow> Re x < Re y
[PROOF STEP]
by simp


[STATEMENT]
lemma complex_of_real_cmod: assumes "x \<ge> 0" shows "complex_of_real (cmod x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (cmod x) = x
[PROOF STEP]
by (metis Reals_cases abs_of_nonneg assms comp_Im_same complex_is_Real_iff complex_of_real_nn_iff norm_of_real zero_complex.simps(2))


[STATEMENT]
lemma arith_prog_0_right [simp]: "arith_prog a 0 = {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog a 0 = {a}
[PROOF STEP]
by (simp add: arith_prog_def)


[STATEMENT]
lemma in_arith_progI [intro]: "[x = a] (mod b) \<Longrightarrow> x \<in> arith_prog a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x = a] (mod int b) \<Longrightarrow> x \<in> arith_prog a b
[PROOF STEP]
by (auto simp: arith_prog_def)


[STATEMENT]
lemma arith_prog_disjoint:
  assumes "[a \<noteq> a'] (mod int b)" and "b > 0"
  shows   "arith_prog a b \<inter> arith_prog a' b = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog a b \<inter> arith_prog a' b = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[a \<noteq> a'] (mod int b)
0 < b

goal (1 subgoal):
 1. arith_prog a b \<inter> arith_prog a' b = {}
[PROOF STEP]
by (auto simp: arith_prog_def cong_def)