:: Some Special Matrices of Real Elements and Their Properties
::  by Xiquan Liang , Fuguo Ge and Xiaopeng Yue
::
:: Received October 19, 2006
:: Copyright (c) 2006-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, NAT_1, MATRIX_1, RELAT_1, XXREAL_0, CARD_1,
      ARYTM_3, LATTICE3, FUNCT_4, FINSEQ_1, TREES_1, COMPLEX1, ARYTM_1,
      FUNCOP_1, QC_LANG1, VECTSP_1, REAL_1, MATRIXR1, ZFMISC_1, MATRIX10,
      FUNCT_7;
 notations COMPLEX1, TARSKI, ZFMISC_1, SUBSET_1, FINSEQ_1, MATRIX_0, ORDINAL1,
      FUNCT_7, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, MATRIXR1,
      RLVECT_1, VECTSP_1, STRUCT_0, MATRIX_3, GROUP_1, MATRIX_1;
 constructors XXREAL_0, REAL_1, BINOP_2, MEMBERED, COMPLEX1, MATRIX_3,
      MATRIX_4, MATRIXR1, RELSET_1, FUNCT_7, NUMBERS;
 registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VECTSP_1, ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
 equalities MATRIX_0, MATRIXR1;
 theorems MATRIX_0, MATRIX_3, MATRIXR1, XREAL_1, ABSVALUE, VECTSP_1, MATRIX_4,
      FINSEQ_1, FINSEQ_3, COMPLEX1, MATRIXC1, XXREAL_0, XREAL_0;
 schemes MATRIX_0;

begin

reserve a,b for Real,
  i,j,n for Nat,
  M,M1,M2,M3,M4 for Matrix of n, REAL;

definition
  let M be Matrix of REAL;
  attr M is Positive means
  :Def1:
  for i,j st [i,j] in Indices M holds M*(i,j) > 0;
  attr M is Negative means
  :Def2:
  for i,j st [i,j] in Indices M holds M*(i,j) < 0;
  attr M is Nonpositive means
  :Def3:
  for i,j st [i,j] in Indices M holds M*(i, j) <= 0;
  attr M is Nonnegative means
  :Def4:
  for i,j st [i,j] in Indices M holds M*(i, j) >= 0;
end;

definition
  let M1,M2 be Matrix of REAL;
  pred M1 is_less_than M2 means

  for i,j st [i,j] in Indices M1 holds M1 *(i,j) < M2*(i,j);
  pred M1 is_less_or_equal_with M2 means

  for i,j st [i,j] in Indices M1 holds M1*(i,j) <= M2*(i,j);
end;

definition
  let M be Matrix of REAL;
  func |:M:| -> Matrix of REAL means
  :Def7:
  len it = len M & width it = width
  M & for i,j holds [i,j] in Indices M implies it*(i,j) = |.M*(i,j).|;
  existence
  proof
    deffunc F(Nat,Nat) = In(|.M*($1,$2).|,REAL);
    consider M1 being Matrix of len M,width M,REAL such that
A1: for i,j st [i,j] in Indices M1 holds M1*(i,j) = F(i,j) from
    MATRIX_0:sch 1;
    take M1;
A2: len M1=len M by MATRIX_0:def 2;
A3: now
      per cases;
      case
A4:     len M= 0;
        then width M1=0 by A2,MATRIX_0:def 3;
        hence width M1=width M by A4,MATRIX_0:def 3;
      end;
      case
        len M>0;
        hence width M1=width M by MATRIX_0:23;
      end;
    end;
    thus len M1 = len M & width M1 = width M by A3,A2;
    let i,j;
    assume
A5:   [i,j] in Indices M;
    dom M = dom M1 by A2,FINSEQ_3:29;
    hence M1*(i,j) = In(|.M*(i,j).|,REAL) by A1,A3,A5
        .= |.M*(i,j).|;
  end;
  uniqueness
  proof
    let M1,M2 be Matrix of REAL;
    assume that
A6: len M1=len M and
A7: width M1 =width M and
A8: for i,j st [i,j] in Indices M holds M1*(i,j)=|.M*(i,j).| and
A9: len M2=len M & width M2 =width M and
A10: for i,j st [i,j] in Indices M holds M2*(i,j)=|.M*(i,j).|;
    now
      let i,j;
      assume
A11:  [i,j] in Indices M1;
A12:  dom M1 = dom M by A6,FINSEQ_3:29;
      hence M1*(i,j)=|.M*(i,j).| by A7,A8,A11
        .=M2*(i,j) by A7,A10,A11,A12;
    end;
    hence thesis by A6,A7,A9,MATRIX_0:21;
  end;
end;

definition
  let n;
  let M;
  redefine func -M -> Matrix of n,REAL;
  coherence
  proof
    len M=n by MATRIX_0:24;
    then
A1: len (-M)=n by MATRIX_3:def 2;
    width M=n by MATRIX_0:24;
    then width (-M)=n by MATRIX_3:def 2;
    hence thesis by A1,MATRIX_0:51;
  end;
end;

definition
  let n;
  let M;
  redefine func |:M:| -> Matrix of n,REAL;
  coherence
  proof
    len M=n by MATRIX_0:24;
    then
A1: len |:M:|=n by Def7;
    width M=n by MATRIX_0:24;
    then width |:M:|=n by Def7;
    hence thesis by A1,MATRIX_0:51;
  end;
end;

definition
  let n;
  let M1,M2;
  redefine func M1+M2 -> Matrix of n,REAL;
  coherence
  proof
A1: width M2=n by MATRIX_0:24;
    width M1=n by MATRIX_0:24;
    then len (M1+M2)=len M1 & width (M1+M2)=width M2 by A1,MATRIX_3:def 3;
    hence thesis by A1,MATRIX_0:24,51;
  end;
end;

definition
  let n;
  let M1,M2;
  redefine func M1-M2 -> Matrix of n,REAL;
  coherence
  proof
    len (M1+ -M2)=len M1 by MATRIX_3:def 3;
    hence thesis by MATRIX_4:def 1;
  end;
end;

definition
  let n;
  let a be Real;
  let M;
  redefine func a*M -> Matrix of n,REAL;
  coherence
  proof
A1: width (a*M)=width M by MATRIXR1:27;
    width M=n & len (a*M)=len M by MATRIXR1:27,MATRIX_0:24;
    hence thesis by A1,MATRIX_0:24,51;
  end;
end;

Lm1: 1 in REAL by XREAL_0:def 1;
Lm2: -1 in REAL by XREAL_0:def 1;

registration
  let n;
  cluster (n,n) --> 1 -> Positive for Matrix of n,REAL;
  coherence
  by MATRIX_0:46,Lm1;
  cluster ((n,n) --> -1) -> Negative for Matrix of n,REAL;
  coherence
  proof let M be Matrix of n,REAL such that
A1: M = (n,n) --> -1;
   let i,j;
   assume [i,j] in Indices M;
    then M*(i,j) = -1 by A1,MATRIX_0:46,Lm2;
   hence thesis;
  end;
  cluster ((n,n) --> -1) -> Nonpositive for Matrix of n,REAL;
  coherence
  by MATRIX_0:46,Lm2;
  cluster ((n,n) --> 1) -> Nonnegative for Matrix of n,REAL;
  coherence
  by MATRIX_0:46,Lm1;
end;

registration
  let n;
  cluster Positive Nonnegative for Matrix of n,REAL;
  existence
  proof
   take (n,n) --> In(1,REAL);
   thus thesis;
  end;
  cluster Negative Nonpositive for Matrix of n,REAL;
  existence
  proof
    take (n,n) --> -In(1,REAL);
   thus thesis;
  end;
end;

registration
  cluster Positive Nonnegative for Matrix of REAL;
  existence
  proof
    take (1,1) --> In(1,REAL);
    thus thesis;
  end;
  cluster Negative Nonpositive for Matrix of REAL;
  existence
  proof
    take (1,1) --> -In(1,REAL);
    thus thesis;
  end;
end;

registration
  let M be Positive Matrix of REAL;
  cluster M@ -> Positive;
  coherence
  proof
    for i,j st [i,j] in Indices (M@) holds (M@)*(i,j) > 0
    proof
      let i,j;
      assume [i,j] in Indices (M@);
      then
A1:   [j,i] in Indices M by MATRIX_0:def 6;
      then (M@)*(i,j) = M*(j,i) by MATRIX_0:def 6;
      hence thesis by A1,Def1;
    end;
    hence thesis;
  end;
end;

registration
  let M be Negative Matrix of REAL;
  cluster M@ -> Negative;
  coherence
  proof
    for i,j st [i,j] in Indices (M@) holds (M@)*(i,j) < 0
    proof
      let i,j;
      assume [i,j] in Indices (M@);
      then
A1:   [j,i] in Indices M by MATRIX_0:def 6;
      then (M@)*(i,j) = M*(j,i) by MATRIX_0:def 6;
      hence thesis by A1,Def2;
    end;
    hence thesis;
  end;
end;

registration
  let M be Nonpositive Matrix of REAL;
  cluster M@ -> Nonpositive;
  coherence
  proof
    for i,j st [i,j] in Indices (M@) holds (M@)*(i,j) <= 0
    proof
      let i,j;
      assume [i,j] in Indices (M@);
      then
A1:   [j,i] in Indices M by MATRIX_0:def 6;
      then (M@)*(i,j) = M*(j,i) by MATRIX_0:def 6;
      hence thesis by A1,Def3;
    end;
    hence thesis;
  end;
end;

registration
  let M be Nonnegative Matrix of REAL;
  cluster M@ -> Nonnegative;
  coherence
  proof
    for i,j st [i,j] in Indices (M@) holds (M@)*(i,j) >= 0
    proof
      let i,j;
      assume [i,j] in Indices (M@);
      then
A1:   [j,i] in Indices M by MATRIX_0:def 6;
      then (M@)*(i,j) = M*(j,i) by MATRIX_0:def 6;
      hence thesis by A1,Def4;
    end;
    hence thesis;
  end;
end;

Lm3: len M1=len M2 & width M1=width M2
proof
  width M1=n & len M1=n by MATRIX_0:24;
  hence thesis by MATRIX_0:24;
end;

theorem
  for x1 be Element of F_Real for x2 be Real st x1 = x2 holds -x1=-x2;

theorem Th2:
  for M being Matrix of REAL st [i,j] in Indices M holds (-M)*(i,j) =-(M*(i,j))
proof
  let M be Matrix of REAL;
  assume [i,j] in Indices M;
  then (-M)*(i,j)= -((MXR2MXF M)*(i,j)) by MATRIX_3:def 2,VECTSP_1:def 5;
  hence thesis by VECTSP_1:def 5;
end;

theorem Th3:
  for M1,M2 be Matrix of REAL st len M1=len M2 & width M1=width M2
  & [i,j] in Indices M1 holds (M1-M2)*(i,j)=(M1*(i,j)) - (M2*(i,j))
proof
  let M1,M2 be Matrix of REAL;
  assume that
A1: len M1=len M2 and
A2: width M1=width M2 and
A3: [i,j] in Indices M1;
A4: 1<=j & j<=width M2 by A2,A3,MATRIXC1:1;
  1<= i & i<=len M2 by A1,A3,MATRIXC1:1;
  then
A5: [i,j] in Indices MXR2MXF M2 by A4,MATRIXC1:1;
  (M1-M2)*(i,j) = ((MXR2MXF M1)+(-(MXR2MXF M2)))*(i,j) by MATRIX_4:def 1
,VECTSP_1:def 5
    .= (MXR2MXF M1)*(i,j)+(-MXR2MXF M2)*(i,j) by A3,MATRIX_3:def 3
    .= (MXR2MXF M1)*(i,j)+-((MXR2MXF M2)*(i,j)) by A5,MATRIX_3:def 2;
  hence thesis by VECTSP_1:def 5;
end;

theorem Th4:
  for M being Matrix of REAL st [i,j] in Indices M holds (a*M)*(i,j
  )=a*(M*(i,j))
proof
  let M be Matrix of REAL;
  a in REAL by XREAL_0:def 1;
  then reconsider aa=a as Element of F_Real by VECTSP_1:def 5;
A1: MXR2MXF(a*M) = MXR2MXF MXF2MXR (aa*(MXR2MXF M)) by MATRIXR1:def 7
    .= aa*(MXR2MXF M);
  assume [i,j] in Indices M;
  then (a*M)*(i,j) = aa*((MXR2MXF M)*(i,j)) by A1,MATRIX_3:def 5,VECTSP_1:def 5
;
  hence thesis by VECTSP_1:def 5;
end;

theorem Th5:
  Indices M = Indices |:M:|
proof
A1: Seg len M = dom M by FINSEQ_1:def 3;
  len |:M:|= len M & width |:M:| =width M by Def7;
  hence thesis by A1,FINSEQ_1:def 3;
end;

theorem
  |:a*M:|=|.a.|*|:M:|
proof
A1: len (a*M)=len M & width (a*M) =width M by MATRIXR1:27;
  len (|.a.|*|:M:|)=len |:M:| by MATRIXR1:27;
  then
A2: len (|.a.|*|:M:|)=len M by Def7;
A3: for i,j st [i,j] in Indices |:a*M:| holds |:a*M:|*(i,j) = (|.a.|*|:M:|)
  *(i,j)
  proof
A4: Indices (a*M) = Indices M by MATRIXR1:28;
A5: Indices (a*M) = Indices M by MATRIXR1:28;
    let i,j;
    assume
A6: [i,j] in Indices |:a*M:|;
A7: Indices |:M:| = Indices M by Th5;
A8: Indices |:a*M:| = Indices (a*M) by Th5;
    then
A9: |:a*M:|*(i,j)=|.(a*M)*(i,j).| by A6,Def7
      .=|.a*(M*(i,j)).| by A6,A8,A4,Th4
      .=|.a.|*|.M*(i,j).| by COMPLEX1:65;
    (|.a.|*|:M:|)*(i,j)=|.a.|*(|:M:|*(i,j)) by A6,A8,A5,Th4,A7
      .=|:a*M:|*(i,j) by A6,A8,A9,A5,Def7;
    hence thesis;
  end;
  width (|.a.|*|:M:|) =width |:M:| by MATRIXR1:27;
  then
A10: width (|.a.|*|:M:|) =width M by Def7;
  len |:a*M:|=len (a*M) & width |:a*M:|=width (a*M) by Def7;
  hence thesis by A1,A2,A10,A3,MATRIX_0:21;
end;

theorem
  M is Negative implies -M is Positive
proof
A1: Indices M=[:Seg n, Seg n:] & Indices (-M)=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A2: M is Negative;
  for i,j st [i,j] in Indices (-M) holds (-M)*(i,j)>0
  proof
    let i,j;
    assume
A3: [i,j] in Indices (-M);
    then M*(i,j)<0 by A2,A1;
    then -M*(i,j)>0 by XREAL_1:58;
    hence thesis by A1,A3,Th2;
  end;
  hence thesis;
end;

theorem
  M1 is Positive & M2 is Positive implies M1+M2 is Positive
proof
A1: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M1 = [:Seg n, Seg n:] & Indices (M1+M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A3: M1 is Positive & M2 is Positive;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (M1+M2);
    then M1*(i,j) > 0 & M2*(i,j) > 0 by A3,A1,A2;
    then M1*(i,j)+M2*(i,j)>0;
    hence thesis by A2,A4,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  -M2 is_less_than M1 implies M1+M2 is Positive
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (-M2)=[:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices (M1+M2)=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A5: -M2 is_less_than M1;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>0
  proof
    let i,j;
    assume
A6: [i,j] in Indices (M1+M2);
    then (-M2)*(i,j)<M1*(i,j) by A5,A3,A4;
    then -M2*(i,j)<M1*(i,j) by A2,A4,A6,Th2;
    then M1*(i,j)+M2*(i,j)>0 by XREAL_1:62;
    hence thesis by A1,A4,A6,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Nonnegative & M2 is Positive implies M1+M2 is Positive
proof
A1: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M1=[:Seg n, Seg n:] & Indices (M1+M2)=[:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A3: M1 is Nonnegative & M2 is Positive;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (M1+M2);
    then M1*(i,j)>=0 & M2*(i,j)>0 by A3,A1,A2;
    then M1*(i,j)+M2*(i,j)>0;
    hence thesis by A2,A4,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| implies
  M1+M2 is Positive
proof
  assume that
A1: M1 is Positive and
A2: M2 is Negative and
A3: |:M2:| is_less_than |:M1:|;
A4: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>0
  proof
    let i,j;
    assume
A7: [i,j] in Indices (M1+M2);
    then [i,j] in Indices |:M2:| by A4,A5,Th5;
    then |:M2:|*(i,j)<|:M1:|*(i,j) by A3;
    then |.M2*(i,j).|<|:M1:|*(i,j) by A4,A5,A7,Def7;
    then |.M2*(i,j).|<|.M1*(i,j).| by A6,A5,A7,Def7;
    then
A8: |.M1*(i,j).|-|.M2*(i,j).|>0 by XREAL_1:50;
    M2*(i,j)<0 by A2,A4,A5,A7;
    then
A9: -(M2*(i,j))=|.M2*(i,j).| by ABSVALUE:def 1;
    M1*(i,j)>0 by A1,A6,A5,A7;
    then M1*(i,j)=|.M1*(i,j).| by ABSVALUE:def 1;
    then M1*(i,j)+M2*(i,j)>0 by A9,A8;
    hence thesis by A6,A5,A7,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Positive & M2 is Negative implies M1-M2 is Positive
proof
  assume
A1: M1 is Positive & M2 is Negative;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M1 = [:Seg n, Seg n:] & Indices (M1-M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
A4: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)>0
  proof
    let i,j;
    assume
A5: [i,j] in Indices (M1-M2);
    then M1*(i,j)>0 & M2*(i,j)<0 by A1,A2,A3;
    then M1*(i,j)-M2*(i,j)>0-0;
    hence thesis by A3,A4,A5,Th3;
  end;
  hence thesis;
end;

theorem
  M2 is_less_than M1 implies M1-M2 is Positive
proof
  assume
A1: M2 is_less_than M1;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M1 = [:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)>0
  proof
    let i,j;
    assume
A6: [i,j] in Indices (M1-M2);
    then M1*(i,j)>M2*(i,j) by A1,A2,A4;
    then M1*(i,j)-M2*(i,j)>0 by XREAL_1:50;
    hence thesis by A4,A5,A3,A6,Th3;
  end;
  hence thesis;
end;

theorem
  a>0 & M is Positive implies a*M is Positive
proof
  assume that
A1: a>0 and
A2: M is Positive;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>0
  proof
    let i,j;
    assume [i,j] in Indices (a*M);
    then
A3: [i,j] in Indices M by MATRIXR1:28;
    then M*(i,j)>0 by A2;
    then a*(M*(i,j))>0 by A1,XREAL_1:129;
    hence thesis by A3,Th4;
  end;
  hence thesis;
end;

theorem
  a<0 & M is Negative implies a*M is Positive
proof
  assume that
A1: a<0 and
A2: M is Negative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)<0 by A2,A3;
    then a*(M*(i,j))>0 by A1,XREAL_1:130;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  M is Positive implies (-M) is Negative
proof
A1: Indices M = [:Seg n, Seg n:] & Indices -M = [:Seg n, Seg n:] by MATRIX_0:24
;
  assume
A2: M is Positive;
  for i,j st [i,j] in Indices (-M) holds (-M)*(i,j)<0
  proof
    let i,j;
    assume
A3: [i,j] in Indices (-M);
    then M*(i,j)>0 by A2,A1;
    then (-1)*(M*(i,j))<0*(-1) by XREAL_1:69;
    then -(M*(i,j))<0;
    hence thesis by A1,A3,Th2;
  end;
  hence thesis;
end;

theorem
  M1 is Negative & M2 is Negative implies M1+M2 is Negative
proof
  assume that
A1: M1 is Negative and
A2: M2 is Negative;
A3: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<0
  proof
    let i,j;
    assume
A6: [i,j] in Indices (M1+M2);
    then M1*(i,j) < 0 by A1,A3,A4;
    then M1*(i,j)+M2*(i,j)<M2*(i,j) by XREAL_1:30;
    then M1*(i,j)+M2*(i,j)<0 by A2,A5,A4,A6;
    hence thesis by A3,A4,A6,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than -M2 implies M1+M2 is Negative
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M2)=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A4: M1 is_less_than -M2;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<0
  proof
    let i,j;
    assume
A5: [i,j] in Indices (M1+M2);
    then M1*(i,j)<(-M2)*(i,j) by A4,A1,A3;
    then M1*(i,j)<-M2*(i,j) by A2,A3,A5,Th2;
    then M1*(i,j)+M2*(i,j)<0 by XREAL_1:61;
    hence thesis by A1,A3,A5,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| implies
  M1+M2 is Negative
proof
  assume that
A1: M1 is Positive and
A2: M2 is Negative and
A3: |:M1:| is_less_than |:M2:|;
A4: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<0
  proof
    let i,j;
    assume
A7: [i,j] in Indices (M1+M2);
    then [i,j] in Indices |:M1:| by A4,A5,Th5;
    then |:M1:|*(i,j)<|:M2:|*(i,j) by A3;
    then |.M1*(i,j).|<|:M2:|*(i,j) by A4,A5,A7,Def7;
    then |.M1*(i,j).|<|.M2*(i,j).| by A6,A5,A7,Def7;
    then
A8: |.M1*(i,j).|-|.M2*(i,j).|<|.M2*(i,j).|-|.M2*(i,j).| by XREAL_1:9;
    M2*(i,j)<0 by A2,A6,A5,A7;
    then
A9: -(M2*(i,j))=|.M2*(i,j).| by ABSVALUE:def 1;
    M1*(i,j)>0 by A1,A4,A5,A7;
    then |.M1*(i,j).|=M1*(i,j) by ABSVALUE:def 1;
    then M1*(i,j)+M2*(i,j)=|.M1*(i,j).|-|.M2*(i,j).| by A9;
    hence thesis by A4,A5,A7,A8,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 implies M1-M2 is Negative
proof
  assume
A1: M1 is_less_than M2;
A2: Indices M1 = [:Seg n, Seg n:] & Indices (M1-M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
A3: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)<0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (M1-M2);
    then M1*(i,j)<M2*(i,j) by A1,A2;
    then M1*(i,j)-M2*(i,j)<0 by XREAL_1:49;
    hence thesis by A2,A3,A4,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is Positive & M2 is Negative implies M2-M1 is Negative
proof
  assume
A1: M1 is Positive & M2 is Negative;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M2 = [:Seg n, Seg n:] & Indices (M2-M1) = [:Seg n, Seg n:] by
MATRIX_0:24;
A4: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)<0
  proof
    let i,j;
    assume
A5: [i,j] in Indices (M2-M1);
    then M1*(i,j)>0 & M2*(i,j)<0 by A1,A2,A3;
    then M2*(i,j)-M1*(i,j)<0;
    hence thesis by A3,A4,A5,Th3;
  end;
  hence thesis;
end;

theorem
  a<0 & M is Positive implies a*M is Negative
proof
  assume that
A1: a<0 and
A2: M is Positive;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)>0 by A2,A3;
    then a*(M*(i,j))<0 by A1,XREAL_1:132;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  a>0 & M is Negative implies a*M is Negative
proof
  assume that
A1: a>0 and
A2: M is Negative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)<0 by A2,A3;
    then a*(M*(i,j))<0 by A1,XREAL_1:132;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  M is Nonnegative implies -M is Nonpositive
proof
A1: Indices M = [:Seg n, Seg n:] & Indices -M = [:Seg n, Seg n:] by MATRIX_0:24
;
  assume
A2: M is Nonnegative;
  for i,j st [i,j] in Indices (-M) holds (-M)*(i,j)<=0
  proof
    let i,j;
    assume
A3: [i,j] in Indices (-M);
    then M*(i,j)>=0 by A2,A1;
    then -(M*(i,j))<=0;
    hence thesis by A1,A3,Th2;
  end;
  hence thesis;
end;

theorem
  M is Negative implies M is Nonpositive;

theorem
  M1 is Nonpositive & M2 is Nonpositive implies M1+M2 is Nonpositive
proof
  assume that
A1: M1 is Nonpositive and
A2: M2 is Nonpositive;
A3: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<=0
  proof
    let i,j;
    assume
A6: [i,j] in Indices (M1+M2);
    then M1*(i,j) <= 0 by A1,A3,A4;
    then
A7: (M1*(i,j))+(M2*(i,j))<=(M2*(i,j)) by XREAL_1:32;
    M2*(i,j) <= 0 by A2,A5,A4,A6;
    hence thesis by A3,A4,A6,A7,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with -M2 implies M1+M2 is Nonpositive
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M2)=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A4: M1 is_less_or_equal_with (-M2);
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<=0
  proof
    let i,j;
    assume
A5: [i,j] in Indices (M1+M2);
    then M1*(i,j)<=(-M2)*(i,j) by A4,A1,A3;
    then M1*(i,j)<=-M2*(i,j) by A2,A3,A5,Th2;
    then M1*(i,j)+M2*(i,j)<=0 by XREAL_1:59;
    hence thesis by A1,A3,A5,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with M2 implies M1-M2 is Nonpositive
proof
  assume
A1: M1 is_less_or_equal_with M2;
A2: Indices M1 = [:Seg n, Seg n:] & Indices (M1-M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
A3: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)<=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (M1-M2);
    then M1*(i,j)<=M2*(i,j) by A1,A2;
    then M1*(i,j)-M2*(i,j)<=0 by XREAL_1:47;
    hence thesis by A2,A3,A4,Th3;
  end;
  hence thesis;
end;

theorem
  a<=0 & M is Positive implies a*M is Nonpositive
proof
  assume that
A1: a<=0 and
A2: M is Positive;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)>0 by A2,A3;
    then a*(M*(i,j))<=0 by A1;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  a>=0 & M is Negative implies a*M is Nonpositive
proof
  assume that
A1: a>=0 and
A2: M is Negative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)<0 by A2,A3;
    then a*(M*(i,j))<=0 by A1;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  a>=0 & M is Nonpositive implies a*M is Nonpositive
proof
  assume that
A1: a>=0 and
A2: M is Nonpositive;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)<=0 by A2,A3;
    then a*(M*(i,j))<=0 by A1;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  a<=0 & M is Nonnegative implies a*M is Nonpositive
proof
  assume that
A1: a<=0 and
A2: M is Nonnegative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)>=0 by A2,A3;
    then a*(M*(i,j))<=0 by A1;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  |:M:| is Nonnegative
proof
  for i,j st [i,j] in Indices |:M:| holds |:M:|*(i,j)>=0
  proof
    let i,j;
    assume
A1: [i,j] in Indices |:M:|;
    Indices |:M:| = Indices M by Th5;
    then |:M:|*(i,j)=|.M*(i,j).| by A1,Def7;
    hence thesis by COMPLEX1:46;
  end;
  hence thesis;
end;

theorem
  M1 is Positive implies M1 is Nonnegative;

theorem
  M is Nonpositive implies (-M) is Nonnegative
proof
A1: Indices M = [:Seg n, Seg n:] & Indices (-M) = [:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A2: M is Nonpositive;
  for i,j st [i,j] in Indices (-M) holds (-M)*(i,j)>=0
  proof
    let i,j;
    assume
A3: [i,j] in Indices (-M);
    then M*(i,j)<=0 by A2,A1;
    then -M*(i,j)>=0;
    hence thesis by A1,A3,Th2;
  end;
  hence thesis;
end;

theorem Th36:
  M1 is Nonnegative & M2 is Nonnegative implies M1+M2 is Nonnegative
proof
A1: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M1 = [:Seg n, Seg n:] & Indices (M1+M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A3: M1 is Nonnegative & M2 is Nonnegative;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (M1+M2);
    then M1*(i,j)>=0 & M2*(i,j)>=0 by A3,A1,A2;
    then (M1*(i,j))+(M2*(i,j))>=0;
    hence thesis by A2,A4,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  -M1 is_less_or_equal_with M2 implies M1+M2 is Nonnegative
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices (-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M2)=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A4: -M1 is_less_or_equal_with M2;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>=0
  proof
    let i,j;
    assume
A5: [i,j] in Indices (M1+M2);
    then (-M1)*(i,j)<=M2*(i,j) by A4,A2,A3;
    then -M1*(i,j)<=M2*(i,j) by A1,A3,A5,Th2;
    then M1*(i,j)+M2*(i,j)>=0 by XREAL_1:60;
    hence thesis by A1,A3,A5,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M2 is_less_or_equal_with M1 implies M1-M2 is Nonnegative
proof
  assume
A1: M2 is_less_or_equal_with M1;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M1 = [:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)>=0
  proof
    let i,j;
    assume
A6: [i,j] in Indices (M1-M2);
    then M1*(i,j)>=M2*(i,j) by A1,A2,A4;
    then M1*(i,j)-M2*(i,j)>=0 by XREAL_1:48;
    hence thesis by A4,A5,A3,A6,Th3;
  end;
  hence thesis;
end;

theorem
  a>=0 & M is Positive implies a*M is Nonnegative
proof
  assume that
A1: a>=0 and
A2: M is Positive;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>=0
  proof
    let i,j;
    assume [i,j] in Indices (a*M);
    then
A3: [i,j] in Indices M by MATRIXR1:28;
    then M*(i,j)>0 by A2;
    then a*(M*(i,j))>=0 by A1;
    hence thesis by A3,Th4;
  end;
  hence thesis;
end;

theorem
  a<=0 & M is Negative implies a*M is Nonnegative
proof
  assume that
A1: a<=0 and
A2: M is Negative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)<0 by A2,A3;
    then a*(M*(i,j))>=0 by A1;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  a<=0 & M is Nonpositive implies a*M is Nonnegative
proof
  assume that
A1: a<=0 and
A2: M is Nonpositive;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)<=0 by A2,A3;
    then a*(M*(i,j))>=0 by A1;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem Th42:
  a>=0 & M is Nonnegative implies a*M is Nonnegative
proof
  assume that
A1: a>=0 and
A2: M is Nonnegative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
  for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>=0
  proof
    let i,j;
    assume
A4: [i,j] in Indices (a*M);
    then M*(i,j)>=0 by A2,A3;
    then a*(M*(i,j))>=0 by A1;
    hence thesis by A3,A4,Th4;
  end;
  hence thesis;
end;

theorem
  a>=0 & b>=0 & M1 is Nonnegative & M2 is Nonnegative implies a*M1+b*M2
  is Nonnegative
proof
  assume a>=0 & b>=0 & M1 is Nonnegative & M2 is Nonnegative;
  then a*M1 is Nonnegative & b*M2 is Nonnegative by Th42;
  hence thesis by Th36;
end;

begin

theorem
  M1 is_less_than M2 implies M1 is_less_or_equal_with M2;

theorem
  M1 is_less_than M2 & M2 is_less_than M3 implies M1 is_less_than M3
proof
A1: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A2: M1 is_less_than M2 & M2 is_less_than M3;
  for i,j st [i,j] in Indices M1 holds M1*(i,j)<M3*(i,j)
  proof
    let i,j;
    assume [i,j] in Indices M1;
    then M1*(i,j)<M2*(i,j) & M2*(i,j)<M3*(i,j) by A2,A1;
    hence thesis by XXREAL_0:2;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 & M3 is_less_than M4 implies (M1+M3) is_less_than ( M2+M4)
proof
A1: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M1 = [:Seg n, Seg n:] & Indices (M1+M3) = [:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A4: M1 is_less_than M2 & M3 is_less_than M4;
  for i,j st [i,j] in Indices (M1+M3) holds (M1+M3)*(i,j)<(M2+M4)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (M1+M3);
    then
A6: (M1+M3)*(i,j)=M1*(i,j)+M3*(i,j) & M2*(i,j)+M4*(i,j)=(M2+M4)*(i,j) by A1,A3,
MATRIXR1:25;
    M1*(i,j)<M2*(i,j) & M3*(i,j)<M4*(i,j) by A4,A2,A3,A5;
    hence thesis by A6,XREAL_1:8;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 implies M1+M3 is_less_than M2+M3
proof
A1: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M3) = [:Seg n, Seg n:] by MATRIX_0:24;
  assume
A4: M1 is_less_than M2;
  for i,j st [i,j] in Indices (M1+M3) holds (M1+M3)*(i,j)<(M2+M3)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (M1+M3);
    then M1*(i,j)<M2*(i,j) by A4,A1,A3;
    then M1*(i,j)+M3*(i,j)<M2*(i,j)+M3*(i,j) by XREAL_1:8;
    then (M1+M3)*(i,j)<M2*(i,j)+M3*(i,j) by A1,A3,A5,MATRIXR1:25;
    hence thesis by A2,A3,A5,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 implies M3-M2 is_less_than M3-M1
proof
  assume
A1: M1 is_less_than M2;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M3-M1) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: width M2=width M3 by Lm3;
A5: Indices M3 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A6: len M1=len M2 & width M1=width M2 by Lm3;
A7: for i,j st [i,j] in Indices (M3-M1) holds (M3-M2)*(i,j)<(M3-M1)*(i,j)
  proof
    let i,j;
    assume
A8: [i,j] in Indices (M3-M1);
    then M1*(i,j)<M2*(i,j) by A1,A2,A3;
    then M3*(i,j)-M2*(i,j)<M3*(i,j)-M1*(i,j) by XREAL_1:15;
    then (M3-M2)*(i,j)<M3*(i,j)-M1*(i,j) by A3,A5,A4,A8,Th3;
    hence thesis by A3,A6,A5,A4,A8,Th3;
  end;
  Indices (M3-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
  hence thesis by A3,A7;
end;

theorem
  |:M1+M2:| is_less_or_equal_with |:M1:|+|:M2:|
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices (M1+M2)=[:Seg n,Seg n:] by MATRIX_0:24;
A3: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices |:M1+M2:| holds |:M1+M2:|*(i,j)<=(|:M1:|+|:
  M2:|)*(i,j)
  proof
    let i,j;
    assume [i,j] in Indices |:M1+M2:|;
    then
A4: [i,j] in Indices (M1+M2) by Th5;
    then [i,j] in Indices |:M1:| by A1,A2,Th5;
    then
A5: (|:M1:|+|:M2:|)*(i,j)=|:M1:|*(i,j)+|:M2:|*(i,j) by MATRIXR1:25
      .=|.M1*(i,j).|+|:M2:|*(i,j) by A1,A2,A4,Def7
      .=|.M1*(i,j).|+|.M2*(i,j).| by A3,A2,A4,Def7;
    |:M1+M2:|*(i,j) =|.(M1+M2)*(i,j).| by A4,Def7
      .=|.M1*(i,j)+M2*(i,j).| by A1,A2,A4,MATRIXR1:25;
    hence thesis by A5,COMPLEX1:56;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with M2 implies (M1-M3) is_less_or_equal_with (M2- M3)
proof
  assume
A1: M1 is_less_or_equal_with M2;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: Indices M2 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A5: Indices (M1-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M3 & width M1=width M3 by Lm3;
  for i,j st [i,j] in Indices (M1-M3) holds (M1-M3)*(i,j)<=(M2-M3)*(i,j)
  proof
    let i,j;
    assume
A7: [i,j] in Indices (M1-M3);
    then M1*(i,j)<=M2*(i,j) by A1,A2,A5;
    then M1*(i,j)-M3*(i,j)<=M2*(i,j)-M3*(i,j) by XREAL_1:9;
    then (M1-M3)*(i,j)<=M2*(i,j)-M3*(i,j) by A2,A5,A6,A7,Th3;
    hence thesis by A5,A4,A3,A7,Th3;
  end;
  hence thesis;
end;

theorem
  (M1-M3) is_less_or_equal_with (M2-M3) implies M1 is_less_or_equal_with M2
proof
  assume
A1: (M1-M3) is_less_or_equal_with (M2-M3);
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: Indices M2 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A5: Indices (M1-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M3 & width M1=width M3 by Lm3;
  for i,j st [i,j] in Indices M1 holds M1*(i,j)<=M2*(i,j)
  proof
    let i,j;
    assume
A7: [i,j] in Indices M1;
    then (M1-M3)*(i,j)<=(M2-M3)*(i,j) by A1,A2,A5;
    then M1*(i,j)-M3*(i,j)<=(M2-M3)*(i,j) by A6,A7,Th3;
    then M1*(i,j)-M3*(i,j)<=M2*(i,j)-M3*(i,j) by A2,A4,A3,A7,Th3;
    then (M1*(i,j)-M3*(i,j))+M3*(i,j)<=(M2*(i,j)-M3*(i,j))+M3*(i,j) by
XREAL_1:6;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with M2-M3 implies M3 is_less_or_equal_with M2-M1
proof
  assume
A1: M1 is_less_or_equal_with M2-M3;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A4: len M2=len M3 & width M2=width M3 by Lm3;
A5: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices M3 holds M3*(i,j)<=(M2-M1)*(i,j)
  proof
    let i,j;
    assume
A7: [i,j] in Indices M3;
    then M1*(i,j)<=(M2-M3)*(i,j) by A1,A2,A3;
    then M1*(i,j)<=M2*(i,j)-M3*(i,j) by A5,A3,A4,A7,Th3;
    then M3*(i,j)<=M2*(i,j)-M1*(i,j) by XREAL_1:11;
    hence thesis by A5,A3,A6,A7,Th3;
  end;
  hence thesis;
end;

theorem
  M1-M2 is_less_or_equal_with M3 implies M1-M3 is_less_or_equal_with M2
proof
  assume
A1: M1-M2 is_less_or_equal_with M3;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: len M1=len M3 & width M1=width M3 by Lm3;
A4: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M1-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices (M1-M3) holds (M1-M3)*(i,j)<=M2*(i,j)
  proof
    let i,j;
    assume
A7: [i,j] in Indices (M1-M3);
    then (M1-M2)*(i,j)<=M3*(i,j) by A1,A4,A5;
    then M1*(i,j)-M2*(i,j)<=M3*(i,j) by A2,A5,A6,A7,Th3;
    then M1*(i,j)-M3*(i,j)<=M2*(i,j) by XREAL_1:12;
    hence thesis by A2,A5,A3,A7,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 & M3 is_less_or_equal_with M4 implies M1-M4
  is_less_than M2-M3
proof
  assume
A1: M1 is_less_than M2 & M3 is_less_or_equal_with M4;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M2 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A4: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: width M2=width M3 by Lm3;
A6: Indices (M1-M4) = [:Seg n, Seg n:] by MATRIX_0:24;
A7: len M1=len M4 & width M1=width M4 by Lm3;
  for i,j st [i,j] in Indices (M1-M4) holds (M1-M4)*(i,j)<(M2-M3)*(i,j)
  proof
    let i,j;
    assume
A8: [i,j] in Indices (M1-M4);
    then M1*(i,j)<M2*(i,j) & M3*(i,j)<=M4*(i,j) by A1,A2,A4,A6;
    then M1*(i,j)-M4*(i,j)<M2*(i,j)-M3*(i,j) by XREAL_1:14;
    then (M1-M4)*(i,j)<M2*(i,j)-M3*(i,j) by A2,A6,A7,A8,Th3;
    hence thesis by A6,A3,A5,A8,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with M2 & M3 is_less_than M4 implies M1-M4
  is_less_than M2-M3
proof
  assume
A1: M1 is_less_or_equal_with M2 & M3 is_less_than M4;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M2 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A4: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: width M2=width M3 by Lm3;
A6: Indices (M1-M4) = [:Seg n, Seg n:] by MATRIX_0:24;
A7: len M1=len M4 & width M1=width M4 by Lm3;
  for i,j st [i,j] in Indices (M1-M4) holds (M1-M4)*(i,j)<(M2-M3)*(i,j)
  proof
    let i,j;
    assume
A8: [i,j] in Indices (M1-M4);
    then M1*(i,j)<=M2*(i,j) & M3*(i,j)<M4*(i,j) by A1,A2,A4,A6;
    then M1*(i,j)-M4*(i,j)<M2*(i,j)-M3*(i,j) by XREAL_1:15;
    then (M1-M4)*(i,j)<M2*(i,j)-M3*(i,j) by A2,A6,A7,A8,Th3;
    hence thesis by A6,A3,A5,A8,Th3;
  end;
  hence thesis;
end;

theorem
  M1-M2 is_less_or_equal_with M3-M4 implies M1-M3 is_less_or_equal_with M2-M4
proof
A1: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M2 & width M1=width M2 by Lm3;
A7: len M1=len M3 & width M1=width M3 by Lm3;
A8: len M3=len M4 & width M3=width M4 by Lm3;
  assume
A9: M1-M2 is_less_or_equal_with M3-M4;
  for i,j st [i,j] in Indices (M1-M3) holds (M1-M3)*(i,j)<=(M2-M4)*(i,j)
  proof
    let i,j;
    assume
A10: [i,j] in Indices (M1-M3);
    then (M1-M2)*(i,j)<=(M3-M4)*(i,j) by A9,A2,A3;
    then M1*(i,j)-M2*(i,j)<=(M3-M4)*(i,j) by A1,A3,A6,A10,Th3;
    then M1*(i,j)-M2*(i,j)<=M3*(i,j)-M4*(i,j) by A4,A3,A8,A10,Th3;
    then M1*(i,j)-M3*(i,j)<=M2*(i,j)-M4*(i,j) by XREAL_1:16;
    then (M1-M3)*(i,j)<=M2*(i,j)-M4*(i,j) by A1,A3,A7,A10,Th3;
    hence thesis by A5,A3,A6,A8,A7,A10,Th3;
  end;
  hence thesis;
end;

theorem
  M1-M2 is_less_or_equal_with M3-M4 implies M4-M2 is_less_or_equal_with M3-M1
proof
A1: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices M4 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M4-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M3 & width M1=width M3 by Lm3;
A7: len M3=len M4 & width M3=width M4 by Lm3;
A8: len M1=len M2 & width M1=width M2 by Lm3;
  assume
A9: M1-M2 is_less_or_equal_with M3-M4;
  for i,j st [i,j] in Indices (M4-M2) holds (M4-M2)*(i,j)<=(M3-M1)*(i,j)
  proof
    let i,j;
    assume
A10: [i,j] in Indices (M4-M2);
    then (M1-M2)*(i,j)<=(M3-M4)*(i,j) by A9,A3,A5;
    then M1*(i,j)-M2*(i,j)<=(M3-M4)*(i,j) by A1,A5,A8,A10,Th3;
    then M1*(i,j)-M2*(i,j)<=M3*(i,j)-M4*(i,j) by A2,A5,A7,A10,Th3;
    then M4*(i,j)-M2*(i,j)<=M3*(i,j)-M1*(i,j) by XREAL_1:17;
    then (M4-M2)*(i,j)<=M3*(i,j)-M1*(i,j) by A4,A5,A8,A7,A6,A10,Th3;
    hence thesis by A2,A5,A6,A10,Th3;
  end;
  hence thesis;
end;

theorem
  M1-M2 is_less_or_equal_with M3-M4 implies M4-M3 is_less_or_equal_with M2-M1
proof
A1: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M4 = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices (M4-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A7: len M3=len M4 & width M3=width M4 by Lm3;
A8: len M1=len M2 & width M1=width M2 by Lm3;
  assume
A9: M1-M2 is_less_or_equal_with M3-M4;
  for i,j st [i,j] in Indices (M4-M3) holds (M4-M3)*(i,j)<=(M2-M1)*(i,j)
  proof
    let i,j;
    assume
A10: [i,j] in Indices (M4-M3);
    then (M1-M2)*(i,j)<=(M3-M4)*(i,j) by A9,A5,A6;
    then M1*(i,j)-M2*(i,j)<=(M3-M4)*(i,j) by A1,A6,A8,A10,Th3;
    then M1*(i,j)-M2*(i,j)<=M3*(i,j)-M4*(i,j) by A4,A6,A7,A10,Th3;
    then M4*(i,j)-M3*(i,j)<=M2*(i,j)-M1*(i,j) by XREAL_1:18;
    then (M4-M3)*(i,j)<=M2*(i,j)-M1*(i,j) by A3,A6,A7,A10,Th3;
    hence thesis by A2,A6,A8,A10,Th3;
  end;
  hence thesis;
end;

theorem
  M1+M2 is_less_or_equal_with M3 implies M1 is_less_or_equal_with M3-M2
proof
  assume
A1: M1+M2 is_less_or_equal_with M3;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M3 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices M1 holds M1*(i,j)<=(M3-M2)*(i,j)
  proof
    let i,j;
    assume
A6: [i,j] in Indices M1;
    then (M1+M2)*(i,j)<=M3*(i,j) by A1,A2,A4;
    then M1*(i,j)+M2*(i,j)<=M3*(i,j) by A6,MATRIXR1:25;
    then M1*(i,j)<=M3*(i,j)-M2*(i,j) by XREAL_1:19;
    hence thesis by A2,A5,A3,A6,Th3;
  end;
  hence thesis;
end;

theorem
  M1+M2 is_less_or_equal_with M3+M4 implies M1-M3 is_less_or_equal_with M4-M2
proof
  assume
A1: M1+M2 is_less_or_equal_with M3+M4;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M4 by Lm3;
A4: Indices (M1+M2)=[:Seg n,Seg n:] by MATRIX_0:24;
A5: Indices M4=[:Seg n, Seg n:] & len M2=len M4 by Lm3,MATRIX_0:24;
A6: Indices M3=[:Seg n, Seg n:] by MATRIX_0:24;
A7: Indices (M1-M3)=[:Seg n,Seg n:] by MATRIX_0:24;
A8: len M1=len M3 & width M1=width M3 by Lm3;
  for i,j st [i,j] in Indices (M1-M3) holds (M1-M3)*(i,j)<=(M4-M2)*(i,j)
  proof
    let i,j;
    assume
A9: [i,j] in Indices (M1-M3);
    then (M1+M2)*(i,j)<=(M3+M4)*(i,j) by A1,A4,A7;
    then M1*(i,j)+M2*(i,j)<=(M3+M4)*(i,j) by A2,A7,A9,MATRIXR1:25;
    then M1*(i,j)+M2*(i,j)<=M3*(i,j)+M4*(i,j) by A6,A7,A9,MATRIXR1:25;
    then M1*(i,j)-M3*(i,j)<=M4*(i,j)-M2*(i,j) by XREAL_1:21;
    then (M1-M3)*(i,j)<=M4*(i,j)-M2*(i,j) by A2,A7,A8,A9,Th3;
    hence thesis by A7,A5,A3,A9,Th3;
  end;
  hence thesis;
end;

theorem
  M1+M2 is_less_or_equal_with M3-M4 implies M1+M4 is_less_or_equal_with M3-M2
proof
  assume
A1: M1+M2 is_less_or_equal_with M3-M4;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M2)=[:Seg n,Seg n:] by MATRIX_0:24;
A4: Indices (M1+M4)=[:Seg n,Seg n:] by MATRIX_0:24;
A5: len M2=len M3 & width M2=width M3 by Lm3;
A6: Indices M3=[:Seg n, Seg n:] by MATRIX_0:24;
A7: len M3=len M4 & width M3=width M4 by Lm3;
  for i,j st [i,j] in Indices (M1+M4) holds (M1+M4)*(i,j)<=(M3-M2)*(i,j)
  proof
    let i,j;
    assume
A8: [i,j] in Indices (M1+M4);
    then (M1+M2)*(i,j)<=(M3-M4)*(i,j) by A1,A3,A4;
    then M1*(i,j)+M2*(i,j)<=(M3-M4)*(i,j) by A2,A4,A8,MATRIXR1:25;
    then M1*(i,j)+M2*(i,j)<=M3*(i,j)-M4*(i,j) by A6,A4,A7,A8,Th3;
    then M1*(i,j)+M4*(i,j)<=M3*(i,j)-M2*(i,j) by XREAL_1:22;
    then (M1+M4)*(i,j)<=M3*(i,j)-M2*(i,j) by A2,A4,A8,MATRIXR1:25;
    hence thesis by A6,A4,A5,A8,Th3;
  end;
  hence thesis;
end;

theorem
  M1-M2 is_less_or_equal_with M3+M4 implies M1-M4 is_less_or_equal_with M3+M2
proof
  assume
A1: M1-M2 is_less_or_equal_with M3+M4;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1-M2)=[:Seg n,Seg n:] by MATRIX_0:24;
A4: Indices (M1-M4)=[:Seg n,Seg n:] by MATRIX_0:24;
A5: len M1=len M2 & width M1=width M2 by Lm3;
A6: Indices M3=[:Seg n, Seg n:] by MATRIX_0:24;
A7: len M1=len M4 & width M1=width M4 by Lm3;
  for i,j st [i,j] in Indices (M1-M4) holds (M1-M4)*(i,j)<=(M3+M2)*(i,j)
  proof
    let i,j;
    assume
A8: [i,j] in Indices (M1-M4);
    then (M1-M2)*(i,j)<=(M3+M4)*(i,j) by A1,A3,A4;
    then M1*(i,j)-M2*(i,j)<=(M3+M4)*(i,j) by A2,A4,A5,A8,Th3;
    then M1*(i,j)-M2*(i,j)<=M3*(i,j)+M4*(i,j) by A6,A4,A8,MATRIXR1:25;
    then M1*(i,j)-M4*(i,j)<=M3*(i,j)+M2*(i,j) by XREAL_1:23;
    then (M1-M4)*(i,j)<=M3*(i,j)+M2*(i,j) by A2,A4,A7,A8,Th3;
    hence thesis by A6,A4,A8,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with M2 implies -M2 is_less_or_equal_with -M1
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (-M2)=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A4: M1 is_less_or_equal_with M2;
  for i,j st [i,j] in Indices (-M2) holds (-M2)*(i,j)<=(-M1)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (-M2);
    then M1*(i,j)<=M2*(i,j) by A4,A1,A3;
    then -M2*(i,j)<=-M1*(i,j) by XREAL_1:24;
    then (-M2)*(i,j)<=-M1*(i,j) by A2,A3,A5,Th2;
    hence thesis by A1,A3,A5,Th2;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with -M2 implies M2 is_less_or_equal_with -M1
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A2: M1 is_less_or_equal_with -M2;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(-M1)*(i,j)
  proof
    let i,j;
    assume
A3: [i,j] in Indices M2;
    then M1*(i,j)<=(-M2)*(i,j) by A2,A1;
    then M1*(i,j)<=-M2*(i,j) by A3,Th2;
    then M2*(i,j)<=-M1*(i,j) by XREAL_1:25;
    hence thesis by A1,A3,Th2;
  end;
  hence thesis;
end;

theorem
  -M2 is_less_or_equal_with M1 implies -M1 is_less_or_equal_with M2
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (-M2)=[:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices (-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A5: -M2 is_less_or_equal_with M1;
  for i,j st [i,j] in Indices (-M1) holds (-M1)*(i,j)<=M2*(i,j)
  proof
    let i,j;
    assume
A6: [i,j] in Indices (-M1);
    then (-M2)*(i,j)<=M1*(i,j) by A5,A4,A3;
    then -M2*(i,j)<=M1*(i,j) by A2,A4,A6,Th2;
    then -M1*(i,j)<=M2*(i,j) by XREAL_1:26;
    hence thesis by A1,A4,A6,Th2;
  end;
  hence thesis;
end;

theorem
  M1 is Positive implies M2 is_less_than M2+M1
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A2: M1 is Positive;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M2+M1)*(i,j)
  proof
    let i,j;
    assume
A3: [i,j] in Indices M2;
    then M1*(i,j)>0 by A2,A1;
    then M2*(i,j)<M2*(i,j)+M1*(i,j) by XREAL_1:29;
    hence thesis by A3,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Negative implies M1+M2 is_less_than M2
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices (M1+M2)=[:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A2: M1 is Negative;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<M2*(i,j)
  proof
    let i,j;
    assume
A3: [i,j] in Indices (M1+M2);
    then M1*(i,j)<0 by A2,A1;
    then M1*(i,j)+M2*(i,j)<M2*(i,j) by XREAL_1:30;
    hence thesis by A1,A3,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Nonnegative implies M2 is_less_or_equal_with M1+M2
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A2: M1 is Nonnegative;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(M1+M2)*(i,j)
  proof
    let i,j;
    assume
A3: [i,j] in Indices M2;
    then M1*(i,j)>=0 by A2,A1;
    then M2*(i,j)<=M1*(i,j)+M2*(i,j) by XREAL_1:31;
    hence thesis by A1,A3,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Nonpositive implies M1+M2 is_less_or_equal_with M2
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices (M1+M2)=[:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A2: M1 is Nonpositive;
  for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<=M2*(i,j)
  proof
    let i,j;
    assume
A3: [i,j] in Indices (M1+M2);
    then M1*(i,j)<=0 by A2,A1;
    then M1*(i,j)+M2*(i,j)<=M2*(i,j) by XREAL_1:32;
    hence thesis by A1,A3,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Nonpositive & M3 is_less_or_equal_with M2 implies M3+M1
  is_less_or_equal_with M2
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3=[:Seg n, Seg n:] & Indices (M3+M1)=[:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A3: M1 is Nonpositive & M3 is_less_or_equal_with M2;
  for i,j st [i,j] in Indices (M3+M1) holds (M3+M1)*(i,j)<=M2*(i,j)
  proof
    let i,j;
    assume
A4: [i,j] in Indices (M3+M1);
    then M1*(i,j)<=0 & M3*(i,j)<=M2*(i,j) by A3,A1,A2;
    then M3*(i,j)+M1*(i,j)<=M2*(i,j) by XREAL_1:35;
    hence thesis by A2,A4,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Nonpositive & M3 is_less_than M2 implies M3+M1 is_less_than M2
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3=[:Seg n, Seg n:] & Indices (M3+M1)=[:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A3: M1 is Nonpositive & M3 is_less_than M2;
  for i,j st [i,j] in Indices (M3+M1) holds (M3+M1)*(i,j)<M2*(i,j)
  proof
    let i,j;
    assume
A4: [i,j] in Indices (M3+M1);
    then M1*(i,j)<=0 & M3*(i,j)<M2*(i,j) by A3,A1,A2;
    then M3*(i,j)+M1*(i,j)<M2*(i,j) by XREAL_1:36;
    hence thesis by A2,A4,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Negative & M3 is_less_or_equal_with M2 implies M3+M1 is_less_than M2
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3=[:Seg n, Seg n:] & Indices (M3+M1)=[:Seg n, Seg n:] by
MATRIX_0:24;
  assume
A3: M1 is Negative & M3 is_less_or_equal_with M2;
  for i,j st [i,j] in Indices (M3+M1) holds (M3+M1)*(i,j)<M2*(i,j)
  proof
    let i,j;
    assume
A4: [i,j] in Indices (M3+M1);
    then M1*(i,j)<0 & M3*(i,j)<=M2*(i,j) by A3,A1,A2;
    then M3*(i,j)+M1*(i,j)<M2*(i,j) by XREAL_1:37;
    hence thesis by A2,A4,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Nonnegative & M2 is_less_or_equal_with M3 implies M2
  is_less_or_equal_with M1+M3
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A2: M1 is Nonnegative & M2 is_less_or_equal_with M3;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(M1+M3)*(i,j)
  proof
    let i,j;
    assume
A3: [i,j] in Indices M2;
    then M1*(i,j)>=0 & M2*(i,j)<=M3*(i,j) by A2,A1;
    then M2*(i,j)<=M1*(i,j)+M3*(i,j) by XREAL_1:38;
    hence thesis by A1,A3,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Positive & M2 is_less_or_equal_with M3 implies M2 is_less_than M1+M3
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A2: M1 is Positive & M2 is_less_or_equal_with M3;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M1+M3)*(i,j)
  proof
    let i,j;
    assume
A3: [i,j] in Indices M2;
    then M1*(i,j)>0 & M2*(i,j)<=M3*(i,j) by A2,A1;
    then M2*(i,j)<M1*(i,j)+M3*(i,j) by XREAL_1:39;
    hence thesis by A1,A3,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Nonnegative & M2 is_less_than M3 implies M2 is_less_than M1+M3
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
  assume
A2: M1 is Nonnegative & M2 is_less_than M3;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M1+M3)*(i,j)
  proof
    let i,j;
    assume
A3: [i,j] in Indices M2;
    then M1*(i,j)>=0 & M2*(i,j)<M3*(i,j) by A2,A1;
    then M2*(i,j)<M1*(i,j)+M3*(i,j) by XREAL_1:40;
    hence thesis by A1,A3,MATRIXR1:25;
  end;
  hence thesis;
end;

theorem
  M1 is Nonnegative implies M2-M1 is_less_or_equal_with M2
proof
  assume
A1: M1 is Nonnegative;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M2-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)<=M2*(i,j)
  proof
    let i,j;
    assume
A6: [i,j] in Indices (M2-M1);
    then M1*(i,j)>=0 by A1,A2,A4;
    then M2*(i,j)-M1*(i,j)<=M2*(i,j) by XREAL_1:43;
    hence thesis by A4,A5,A3,A6,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is Positive implies M2-M1 is_less_than M2
proof
  assume
A1: M1 is Positive;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M2-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)<M2*(i,j)
  proof
    let i,j;
    assume
A6: [i,j] in Indices (M2-M1);
    then M1*(i,j)>0 by A1,A2,A4;
    then M2*(i,j)-M1*(i,j)<M2*(i,j) by XREAL_1:44;
    hence thesis by A4,A5,A3,A6,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is Nonpositive implies M2 is_less_or_equal_with M2-M1
proof
  assume
A1: M1 is Nonpositive;
A2: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(M2-M1)*(i,j)
  proof
    let i,j;
    assume
A4: [i,j] in Indices M2;
    then M1*(i,j)<=0 by A1,A2;
    then M2*(i,j)<=M2*(i,j)-M1*(i,j) by XREAL_1:45;
    hence thesis by A3,A4,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is Negative implies M2 is_less_than M2-M1
proof
  assume
A1: M1 is Negative;
A2: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M2-M1)*(i,j)
  proof
    let i,j;
    assume
A4: [i,j] in Indices M2;
    then M1*(i,j)<0 by A1,A2;
    then M2*(i,j)<M2*(i,j)-M1*(i,j) by XREAL_1:46;
    hence thesis by A3,A4,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with M2 implies M2-M1 is Nonnegative
proof
  assume
A1: M1 is_less_or_equal_with M2;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M2-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)>=0
  proof
    let i,j;
    assume
A6: [i,j] in Indices (M2-M1);
    then M1*(i,j)<=M2*(i,j) by A1,A2,A4;
    then M2*(i,j)-M1*(i,j)>=0 by XREAL_1:48;
    hence thesis by A4,A5,A3,A6,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is Nonnegative & M2 is_less_than M3 implies M2-M1 is_less_than M3
proof
  assume
A1: M1 is Nonnegative & M2 is_less_than M3;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M2=[:Seg n, Seg n:] & Indices (M2-M1)=[:Seg n, Seg n:] by
MATRIX_0:24;
A4: len M1=len M2 & width M1=width M2 by Lm3;
  for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)<M3*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (M2-M1);
    then M1*(i,j)>=0 & M2*(i,j)<M3*(i,j) by A1,A2,A3;
    then M2*(i,j)-M1*(i,j)<M3*(i,j) by XREAL_1:51;
    hence thesis by A3,A4,A5,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is Nonpositive & M2 is_less_or_equal_with M3 implies M2
  is_less_or_equal_with M3-M1
proof
  assume
A1: M1 is Nonpositive & M2 is_less_or_equal_with M3;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: width M1=width M2 & len M2=len M3 by Lm3;
A5: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M3=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(M3-M1)*(i,j)
  proof
    let i,j;
    assume
A7: [i,j] in Indices M2;
    then M1*(i,j)<=0 & M2*(i,j)<=M3*(i,j) by A1,A2,A5;
    then M2*(i,j)<=M3*(i,j)-M1*(i,j) by XREAL_1:52;
    hence thesis by A5,A6,A4,A3,A7,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is Nonpositive & M2 is_less_than M3 implies M2 is_less_than M3-M1
proof
  assume
A1: M1 is Nonpositive & M2 is_less_than M3;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: width M1=width M2 & len M2=len M3 by Lm3;
A5: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M3=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M3-M1)*(i,j)
  proof
    let i,j;
    assume
A7: [i,j] in Indices M2;
    then M1*(i,j)<=0 & M2*(i,j)<M3*(i,j) by A1,A2,A5;
    then M2*(i,j)<M3*(i,j)-M1*(i,j) by XREAL_1:53;
    hence thesis by A5,A6,A4,A3,A7,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is Negative & M2 is_less_or_equal_with M3 implies M2 is_less_than M3-M1
proof
  assume
A1: M1 is Negative & M2 is_less_or_equal_with M3;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: width M1=width M2 & len M2=len M3 by Lm3;
A5: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M3=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
  for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M3-M1)*(i,j)
  proof
    let i,j;
    assume
A7: [i,j] in Indices M2;
    then M1*(i,j)<0 & M2*(i,j)<=M3*(i,j) by A1,A2,A5;
    then M2*(i,j)<M3*(i,j)-M1*(i,j) by XREAL_1:54;
    hence thesis by A5,A6,A4,A3,A7,Th3;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 & a>0 implies a*M1 is_less_than a*M2
proof
  assume that
A1: M1 is_less_than M2 and
A2: a>0;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(a*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)<M2*(i,j) by A1,A3;
    then a*(M1*(i,j))<a*(M2*(i,j)) by A2,XREAL_1:68;
    then
A6: (a*M1)*(i,j)<a*(M2*(i,j)) by A3,A5,Th4;
    [i,j] in Indices M2 by A4,A5,MATRIX_0:24;
    hence thesis by A6,Th4;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 & a>=0 implies a*M1 is_less_or_equal_with a*M2
proof
  assume that
A1: M1 is_less_than M2 and
A2: a>=0;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<=(a*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)<M2*(i,j) by A1,A3;
    then a*(M1*(i,j))<=a*(M2*(i,j)) by A2,XREAL_1:64;
    then
A6: (a*M1)*(i,j)<=a*(M2*(i,j)) by A3,A5,Th4;
    [i,j] in Indices M2 by A4,A5,MATRIX_0:24;
    hence thesis by A6,Th4;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 & a<0 implies a*M2 is_less_than a*M1
proof
  assume that
A1: M1 is_less_than M2 and
A2: a<0;
A3: Indices (a*M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M2) holds (a*M2)*(i,j)<(a*M1)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M2);
    then
A6: [i,j] in Indices M1 by A4,MATRIX_0:24;
    then M1*(i,j)<M2*(i,j) by A1;
    then a*(M2*(i,j))<a*(M1*(i,j)) by A2,XREAL_1:69;
    then (a*M2)*(i,j)<a*(M1*(i,j)) by A3,A5,Th4;
    hence thesis by A6,Th4;
  end;
  hence thesis;
end;

theorem
  M1 is_less_than M2 & a<=0 implies a*M2 is_less_or_equal_with a*M1
proof
  assume that
A1: M1 is_less_than M2 and
A2: a<=0;
A3: Indices (a*M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M2) holds (a*M2)*(i,j)<=(a*M1)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M2);
    then
A6: [i,j] in Indices M1 by A4,MATRIX_0:24;
    then M1*(i,j)<M2*(i,j) by A1;
    then a*(M2*(i,j))<=a*(M1*(i,j)) by A2,XREAL_1:65;
    then (a*M2)*(i,j)<=a*(M1*(i,j)) by A3,A5,Th4;
    hence thesis by A6,Th4;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with M2 & a>=0 implies a*M1 is_less_or_equal_with a*M2
proof
  assume that
A1: M1 is_less_or_equal_with M2 and
A2: a>=0;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<=(a*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)<=M2*(i,j) by A1,A3;
    then a*(M1*(i,j))<=a*(M2*(i,j)) by A2,XREAL_1:64;
    then
A6: (a*M1)*(i,j)<=a*(M2*(i,j)) by A3,A5,Th4;
    [i,j] in Indices M2 by A4,A5,MATRIX_0:24;
    hence thesis by A6,Th4;
  end;
  hence thesis;
end;

theorem
  M1 is_less_or_equal_with M2 & a<=0 implies a*M2 is_less_or_equal_with a*M1
proof
  assume that
A1: M1 is_less_or_equal_with M2 and
A2: a<=0;
A3: Indices (a*M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M2) holds (a*M2)*(i,j)<=(a*M1)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M2);
    then
A6: [i,j] in Indices M1 by A4,MATRIX_0:24;
    then M1*(i,j)<=M2*(i,j) by A1;
    then a*(M2*(i,j))<=a*(M1*(i,j)) by A2,XREAL_1:65;
    then (a*M2)*(i,j)<=a*(M1*(i,j)) by A3,A5,Th4;
    hence thesis by A6,Th4;
  end;
  hence thesis;
end;

theorem
  a>=0 & a<=b & M1 is Nonnegative & M1 is_less_or_equal_with M2 implies
  a*M1 is_less_or_equal_with b*M2
proof
  assume that
A1: a>=0 & a<=b and
A2: M1 is Nonnegative & M1 is_less_or_equal_with M2;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<=(b*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)>=0 & M1*(i,j)<=M2*(i,j) by A2,A3;
    then a*(M1*(i,j))<=b*(M2*(i,j)) by A1,XREAL_1:66;
    then (a*M1)*(i,j)<=b*(M2*(i,j)) by A3,A5,Th4;
    hence thesis by A4,A3,A5,Th4;
  end;
  hence thesis;
end;

theorem
  a<=0 & b<=a & M1 is Nonpositive & M2 is_less_or_equal_with M1 implies
  a*M1 is_less_or_equal_with b*M2
proof
  assume that
A1: a<=0 & b<=a and
A2: M1 is Nonpositive & M2 is_less_or_equal_with M1;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<=(b*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)<=0 & M2*(i,j)<=M1*(i,j) by A2,A4,A3;
    then a*(M1*(i,j))<=b*(M2*(i,j)) by A1,XREAL_1:67;
    then (a*M1)*(i,j)<=b*(M2*(i,j)) by A3,A5,Th4;
    hence thesis by A4,A3,A5,Th4;
  end;
  hence thesis;
end;

theorem
  a<0 & b<=a & M1 is Negative & M2 is_less_than M1 implies a*M1
  is_less_than b*M2
proof
  assume that
A1: a<0 & b<=a and
A2: M1 is Negative & M2 is_less_than M1;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(b*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)<0 & M2*(i,j)<M1*(i,j) by A2,A4,A3;
    then a*(M1*(i,j))<b*(M2*(i,j)) by A1,XREAL_1:70;
    then (a*M1)*(i,j)<b*(M2*(i,j)) by A3,A5,Th4;
    hence thesis by A4,A3,A5,Th4;
  end;
  hence thesis;
end;

theorem
  a>=0 & a<b & M1 is Nonnegative & M1 is_less_than M2 implies a*M1
  is_less_than b*M2
proof
  assume that
A1: a>=0 & a<b and
A2: M1 is Nonnegative & M1 is_less_than M2;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(b*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)>=0 & M1*(i,j)<M2*(i,j) by A2,A3;
    then a*(M1*(i,j))<b*(M2*(i,j)) by A1,XREAL_1:96;
    then (a*M1)*(i,j)<b*(M2*(i,j)) by A3,A5,Th4;
    hence thesis by A4,A3,A5,Th4;
  end;
  hence thesis;
end;

theorem
  a>=0 & a<b & M1 is Positive & M1 is_less_or_equal_with M2 implies a*M1
  is_less_than b*M2
proof
  assume that
A1: a>=0 & a<b and
A2: M1 is Positive & M1 is_less_or_equal_with M2;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(b*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)>0 & M1*(i,j)<=M2*(i,j) by A2,A3;
    then a*(M1*(i,j))<b*(M2*(i,j)) by A1,XREAL_1:97;
    then (a*M1)*(i,j)<b*(M2*(i,j)) by A3,A5,Th4;
    hence thesis by A4,A3,A5,Th4;
  end;
  hence thesis;
end;

theorem
  a>0 & a<=b & M1 is Positive & M1 is_less_than M2 implies a*M1
  is_less_than b*M2
proof
  assume that
A1: a>0 & a<=b and
A2: M1 is Positive & M1 is_less_than M2;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
  for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(b*M2)*(i,j)
  proof
    let i,j;
    assume
A5: [i,j] in Indices (a*M1);
    then M1*(i,j)>0 & M1*(i,j)<M2*(i,j) by A2,A3;
    then a*(M1*(i,j))<b*(M2*(i,j)) by A1,XREAL_1:98;
    then (a*M1)*(i,j)<b*(M2*(i,j)) by A3,A5,Th4;
    hence thesis by A4,A3,A5,Th4;
  end;
  hence thesis;
end;