Library Subsets.Finite_table

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Support for finite tables.

Description

Finite tables are rectangular finite families of finite families, ie functions from some ordinal types 'I_m and 'I_n to any type E. For instance, they can represent matrices. But the present module only provides results related to the finite nature of ordinals, no algebraic structure is assumed on the support type E.

Additional notations

  • 'E^{m,n} is for ('E^n)^m, for any type E; it is also 'I_m 'I_n E, and 'I_m 'E^n;
  • 'E^[n] is for 'E^{n,n}.

Support for operations on finite tables

Naming rules:
  • functions having finite tables as input and/or output have a name with suffix "T", eg brT, castT and mapT;
  • functions having row finite tables as input and/or output have a name with suffix "Tr", eg castTr and permutTr;
  • functions having column finite tables as input and/or output have a name with suffix "Tc", eg castTc and permutTc.
Let E be any type. Let PE be a subset of E. Let x, x00, x01, x10 and x11 be in E. Let R be an n-family, and C be an m-family. Let M and N be tables of m×n items of E, a.k.a. (m, n)-tables (of E). Item M i j, a.k.a. item (i, j), is said to be in i-th row and j-th column of table M.

Constructors

  • constT m n x is the (m, n)-table with all items equal to x.
  • blk1T x00 is the (1, 1)-table with only item x.
  • blk2T x00 x01 x10 x11 is the (2, 2)-table with items x00 and x01 in the first row, and x10 and x11 in the second row, in that order.

Destructors

  • row M i is the n-family made of the i-th row of M.
  • col M j is the m-family made of the j-th column of M.

Predicates

Let P be a predicate on 'I_m and 'I_n.
  • PAT P states that P i j holds for all i and j.
  • PET P states that there exists some i and j such that P i j holds.
Let Q also be a predicate on 'I_m and 'I_n.
  • notT P is the complementary predicate of P, ie associating ¬ P i j to each i and j.
  • andT P Q is the intersection predicate of P and Q, ie associating P i j Q i j to each i and j.
  • orT P Q is the union predicate of P and Q, ie associating P i j Q i j to each i and j.
  • impT P Q associates P i j Q i j to each i and j.
  • iffT P Q associates P i j Q i j to each i and j.
Let R be a binary relation on E.
  • brAT R M N states that R (M i j) (N i j) holds for all i and j.
  • brET R M N states that there exists some i and j such that R (M i j) (N i j) holds.
  • eqAT and eqET are the specializations of brAT and brET for equality.
  • neqAT and neqET are the specializations of brAT and brET for the negation of equality.
  • same_funT is the specialization of brAT for extensional equality of functions.
  • eqT M x associates equality M i j = x to each i and j.
  • neqT M x associates inequality M i j x to each i and j.
  • inT x M states that x is some item of M.
  • inclT M PE states that all items of M belong to PE.
  • invalT M1 M2 states that all items of M1 appear in M2. Warning: in the presence of doubles in M1, we may have invalT M1 M2 with m2 < m1 or n2 < n1.
  • eqPT P M N states that M and N are equal when P holds.
  • neqPT P M N states that there exists some i and j such that M i j and N i j are distinct and P i j holds.
  • eqxTr M N i0 states that M and N are equal except for i0-th row.
  • eqxTc M N j0 states that M and N are equal except for j0-th column.
  • eqxT M N i0 j0 states that M and N are equal except for i0-th row and j0-th column.
  • neqxTr M N i0 states that there exists some i distinct from i0 such that M i and N i are distinct.
  • neqxTc M N j0 states that there exists some j distinct from j0 such that fun i M i j and fun i N i j0 are distinct.
  • neqxT M N j0 states that there exists some i distinct from i0 and some j distinct from j0 such that M i j and N i j0 are distinct.

Operators

Let M1 be an (m1, n)-table, and Hm be a proof of m1 = m2.
  • castTr Hm M1 is the (m2, n)-table made of the items of M1, in the same order.
Let M1 be an (m, n1)-table, and Hn be a proof of n1 = n2.
  • castTc Hn M1 is the (m, n2)-table made of the items of M1, in the same order.
Let M1 be an (m1, n1)-table.
  • castT Hm Hn M1 is the (m2, n2)-table made of the items of M1, in the same order.
  • flipT M is the (n, m)-table made of the items of M by switching the dimensions.
Let M12 be an (m1 + m2, n)-table.
  • upT M12 is the (m1, n)-table made of the m1 first rows of M12, in the same order.
  • downT M12 is the (m2, n)-table made of the m2 last rows of M12, in the same order.
Let M1 be an (m1, n)-table, and M2 be an (m2, n)-table.
  • concatTr M1 M2 is the (m1 + m2, n)-table with rows of M1, then rows of M2, in the same order.
Let M12 be an (m, n1 + n2)-table.
  • leftT M12 is the (m, n1)-table made of the n1 first columns of M12, in the same order.
  • rightT M12 is the (m, n2)-table made of the n2 last columns of M12, in the same order.
Let M1 be an (m, n1)-table, and M2 be an (m, n2)-table.
  • concatTc M1 M2 is the (m, n1 + n2)-table with on each row columns of M1, then columns of M2, in the same order.
Let M12 be an (m1 + m2, n1 + n2)-table.
  • ulT M12 is the (m1, n1)-table made of the m1 first rows and n1 first columns of M12, in the same order.
  • urT M12 is the (m1, n2)-table made of the m1 first rows and n2 last columns of M12, in the same order.
  • dlT M12 is the (m2, n1)-table made of the m2 last rows and n1 first columns of M12, in the same order.
  • drT M12 is the (m2, n2)-table made of the m2 last rows and n2 last columns of M12, in the same order.
Let M11 be an (m1, n1)-table, M12 be an (m1, n2)-table, M21 be an (m2, n1)-table, and M22 be an (m2, n2)-table.
  • concatT M11 M12 M21 M22 is the (m1 + n2, n1 + n2)-table with m1 first rows made of columns of M11 then M12 , and with m2 last rows made of columns of M21 and M22, in the same order.
  • insertTr M R i is the (m.+1, n)-table made of the m×n items of M, in the same order, and R inserted as the i-th row.
  • insertTc M C j is the (m, n.+1)-table made of the m×n items of M, in the same order, and C inserted as the j-th column.
  • insertT M R C x i j is the (m.+1, n.+1)-table made of the m×n items of M, in the same order, R inserted as the i-th row, C inserted as the j-th column, and x inserted as item (i, j).
Let M be an (m.+1, n)-table.
  • skipTr M i is the (m, n)-table made of the items of M, in the same order, except those from the i-th row.
Let M be an (m, n.+1)-table.
  • skipTc M j is the (m, n)-table made of the items of M, in the same order, except those from the j-th column.
Let M be an (m.+1, n.+1)-table.
  • skipT M i j is the (m, n)-table made of the items of M, in the same order, except those from the i-th row and from the j-th column.
  • replaceTr M R i is the (m, n)-table made of the m×n items of M, in the same order, except that the i-th row is replaced by R.
  • replaceTc M C j is the (m, n)-table made of the m×n items of M, in the same order, except that the j-th column is replaced by C.
  • replaceT M R C x i j is the (m, n)-table made of the m×n items of M, in the same order, except that the i-th row is replaced by R, the j-th column is replaced by C and item (i, j) is replaced by x.
Let pi : 'I_[m], and pj : 'I_[n].
Let M be an (m.+1, n)-table.
  • moveTr M i0 i1 is the (m.+1, n)-table made of items of M, in the same order, except that i0-th row is moved to i1-th slot.
Let M be an (m, n.+1)-table.
  • moveTc M j0 j1 is the (m, n.+1)-table made of items of M, in the same order, except that j0-th column is moved to j1-th slot.
Let M be an (m.+1, n.+1)-table.
  • moveT M i0 i1 j0 j1 is the (m.+1, n.+1)-table made of items of M, in the same order, except that i0-th row is moved to i1-th slot, and j0-th column is moved to j1-th slot.
  • transpTr M i0 i1 is the (m, n)-table made of items of M, in the same order, except that i0-th and i1-th rows are exchanged.
  • transpTc M j0 j1 is the (m, n)-table made of items of M, in the same order, except that j0-th and j1-th columns are exchanged.
  • transpT M i0 i1 j0 j1 is the (m, n)-table made of items of M, in the same order, except that i0-th and i1-th rows are exchanged, and j0-th and j1-th columns are exchanged.
Let F be any type. Let f : E F and fij : 'I_m 'I_n E F be functions.
  • mapT f M is the (m, n)-table made of the images by f of the items of M, in the same order.
  • mapijT fij M is the (m, n)-table with f i j (M i j) as item (i, j).

About the API

Definitions and statements are mainly plain-Coq compatible (ie use of Prop instead of bool).

Used logic axioms

Usage

This module may be used through the import of Subsets.Subsets, Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or Lebesgue.Bochner.Bochner_wDep, where it is exported.

From Requisite Require Import stdlib ssr_wMC.

From Numbers Require Import Numbers_wDep.
From Subsets Require Import Subset Function.
From Subsets Require Import Binary_relation ord_compl Finite_family.

Notation "''' E ^ { m , n }" := ('('E^n)^m)
  (at level 8, E at level 2, m at level 2, n at level 2,
    format "''' E ^ { m , n }").
Notation "''' E ^ [ n ]" := ('E^{n,n})
  (at level 8, E at level 2, n at level 2, format "''' E ^ [ n ]").

Section FT_Def0a.

Context {m n : nat}.
Variable P Q : 'Prop^{m,n}.

The prefix "P" stands for Prop, "A" for and "E" for .
Definition PAT : Prop := i j, P i j.
Definition PET : Prop := i j, P i j.

Definition notT : 'Prop^{m,n} := fun i j¬ P i j.
Definition andT : 'Prop^{m,n} := fun i jP i j Q i j.
Definition orT : 'Prop^{m,n} := fun i jP i j Q i j.
Definition impT : 'Prop^{m,n} := fun i jP i j Q i j.
Definition iffT : 'Prop^{m,n} := fun i jP i j Q i j.

End FT_Def0a.

Section FT_Def1a.

Context {m n : nat}.
Variable P : 'Prop^{m,n}.

Lemma PT_dec : { PAT P } + { PET (notT P) }.
Proof.
destruct (classic_dec (PAT P));
    [left | right; apply not_all2_ex2_not_equiv]; easy.
Qed.

Lemma PT_dec_l : (H : PAT P), PT_dec = left H.
Proof.
intros H1; destruct PT_dec as [H2 | H2].
f_equal; apply proof_irrel.
contradict H1; apply not_all2_ex2_not_equiv; easy.
Qed.

Lemma PT_dec_r : (H : PET (notT P)), PT_dec = right H.
Proof.
intros H1; destruct PT_dec as [H2 | H2].
contradict H2; apply not_all2_ex2_not_equiv; easy.
f_equal; apply proof_irrel.
Qed.

End FT_Def1a.

Section FT_Def0b.

Context {E : Type}.
Variable R : E E Prop.

Context {m n : nat}.
Variable M N : 'E^{m,n}.

The prefix "br" stands for "binary relation".
Definition brAT : Prop := PAT (fun i jR (M i j) (N i j)).
Definition brET : Prop := PET (fun i jR (M i j) (N i j)).

End FT_Def0b.

Section FT_Def1b.

Context {E F : Type}.
Variable R : E E Prop.

Context {m n : nat}.
Variable M N : 'E^{m,n}.

Definition brT_dec : {brAT R M N} + {brET (complementary R) M N} :=
  PT_dec (fun i jR (M i j) (N i j)).

Lemma brT_dec_l : (H : brAT R M N), brT_dec = left H.
Proof. intros; apply PT_dec_l. Qed.

Lemma brT_dec_r : (H : brET (complementary R) M N), brT_dec = right H.
Proof. intros; apply PT_dec_r. Qed.

Definition eqAT : Prop := brAT eq M N.
Definition eqET : Prop := brET eq M N.

Definition neqAT : Prop := brAT neq M N.
Definition neqET : Prop := brET neq M N.

Variable f g : '(E F)^{m,n}.

Definition same_funT : Prop := brAT same_fun f g.

End FT_Def1b.

Section FT_Facts0a.

Context {E : Type}.
Context {m n : nat}.

Variable M N : 'E^{m,n}.

Lemma extT : eqAT M N M = N.
Proof. repeat (intro; apply extF); easy. Qed.

Lemma extT_rev : M = N eqAT M N.
Proof. intros H; rewrite H; easy. Qed.

Lemma extT_compat : i j k l, i = k j = l M i j = M k l.
Proof. move=>>; apply f_equal2. Qed.

Lemma nextT : neqET M N M N.
Proof. intros H1 H2; rewrite H2 in H1; destruct H1 as [i [j H]]; easy. Qed.

Lemma nextT_rev : M N neqET M N.
Proof.
intros H; destruct (nextF_rev _ _ H) as [i Hi]; i.
destruct (nextF_rev _ _ Hi) as [j Hj]; j; easy.
Qed.

Lemma nextT_reg : i j k l, M i j M k l i k j l.
Proof.
move=>>; rewrite -not_and_equiv; apply contra_not.
intros [H1 H2]; apply extT_compat; easy.
Qed.

End FT_Facts0a.

Section FT_Facts0b.

Context {E F : Type}.
Context {m n : nat}.

Variable f g : '(E F)^{m,n}.

Lemma fun_extT : same_funT f g f = g.
Proof. intros H; apply extT; do 2 intro; apply fun_ext, H. Qed.

End FT_Facts0b.

Section FT_ops_Def1.

Context {E F : Type}.

Definition constT m n (x : E) : 'E^{m,n} := constF m (constF n x).

Definition blk1T (x00 : E) : 'E^{1,1} := singleF (singleF x00).

Definition blk2T (x00 x01 x10 x11 : E) : 'E^{2,2} :=
  coupleF (coupleF x00 x01) (coupleF x10 x11).

Definition row {m n} (M : 'E^{m,n}) i : 'E^n := M i.
Definition col {m n} (M : 'E^{m,n}) j : 'E^m := M^~ j.

Definition eqT {m n} (M : 'E^{m,n}) x i j : Prop := M i j = x.
Definition neqT {m n} (M : 'E^{m,n}) x i j : Prop := M i j x.

Definition inT {m n} x (M : 'E^{m,n}) : Prop := i j, x = M i j.

Definition inclT {m n} (M : 'E^{m,n}) (PE : E Prop) : Prop :=
   i j, PE (M i j).

Definition invalT {m1 m2 n1 n2} (M1 : 'E^{m1,n1}) (M2 : 'E^{m2,n2}) : Prop :=
  inclT M1 (inT^~ M2).

Definition iffAT {m n} (P Q : 'Prop^{m,n}) := i j, P i j Q i j.

Definition eqPT {m n} (P : 'Prop^{m,n}) (M N : 'E^{m,n}) : Prop :=
   i j, P i j M i j = N i j.
Definition neqPT {m n} (P : 'Prop^{m,n}) (M N : 'E^{m,n}) : Prop :=
   i j, P i j M i j N i j.

Definition eqxTr {m n} (M N : 'E^{m,n}) i0 : Prop := eqxF M N i0.
Definition neqxTr {m n} (M N : 'E^{m,n}) i0 : Prop := neqxF M N i0.

Definition eqxTc {m n} (M N : 'E^{m,n}) j0 : Prop :=
   i, eqxF (M i) (N i) j0.
Definition neqxTc {m n} (M N : 'E^{m,n}) j0 : Prop :=
   i, neqxF (M i) (N i) j0.

Definition eqxT {m n} (M N : 'E^{m,n}) i0 j0 : Prop :=
   i j, i i0 j j0 M i j = N i j.
Definition neqxT {m n} (M N : 'E^{m,n}) i0 j0 : Prop :=
   i j, i i0 j j0 M i j N i j.

Definition castTr {m1 m2 n} Hm (M : 'E^{m1,n}) : 'E^{m2,n} := castF Hm M.

Definition castTc {m n1 n2} Hn (M : 'E^{m,n1}) : 'E^{m,n2} :=
  mapF (castF Hn) M.

Definition castT {m1 m2 n1 n2} Hm Hn (M : 'E^{m1,n1}) : 'E^{m2,n2} :=
  castTr Hm (castTc Hn M).

Definition flipT {m n} (M : 'E^{m,n}) : 'E^{n,m} := fun i jM j i.

Definition widenTr_S {m n} (M : 'E^{m.+1,n}) : 'E^{m,n} := widenF_S M.
Definition liftTr_S {m n} (M : 'E^{m.+1,n}) : 'E^{m,n} := liftF_S M.

Definition widenTc_S {m n} (M : 'E^{m,n.+1}) : 'E^{m,n} :=
  fun iwidenF_S (M i).
Definition liftTc_S {m n} (M : 'E^{m,n.+1}) : 'E^{m,n} :=
  fun iliftF_S (M i).

Definition widenT_S {m n} (M : 'E^{m.+1,n.+1}) : 'E^{m,n} :=
  widenTr_S (widenTc_S M).
Definition liftT_S {m n} (M : 'E^{m.+1,n.+1}) : 'E^{m,n} :=
  liftTr_S (liftTc_S M).

Definition upT {m1 m2 n} (M : 'E^{m1 + m2,n}) : 'E^{m1,n} := firstF M.
Definition downT {m1 m2 n} (M : 'E^{m1 + m2,n}) : 'E^{m2,n} := lastF M.
Definition concatTr
    {m1 m2 n} (M1 : 'E^{m1,n}) (M2 : 'E^{m2,n}) : 'E^{m1 + m2,n} :=
  concatF M1 M2.

Definition leftT {m n1 n2} (M : 'E^{m,n1 + n2}) : 'E^{m,n1} :=
  fun ifirstF (M i).
Definition rightT {m n1 n2} (M : 'E^{m,n1 + n2}) : 'E^{m,n2} :=
  fun ilastF (M i).
Definition concatTc
    {m n1 n2} (M1 : 'E^{m,n1}) (M2 : 'E^{m,n2}) : 'E^{m,n1 + n2} :=
  fun iconcatF (M1 i) (M2 i).

Definition ulT {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}) : 'E^{m1,n1} :=
  upT (leftT M).
Definition urT {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}) : 'E^{m1,n2} :=
  upT (rightT M).
Definition dlT {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}) : 'E^{m2,n1} :=
  downT (leftT M).
Definition drT {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}) : 'E^{m2,n2} :=
  downT (rightT M).
Definition concatT
    {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
    (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}) : 'E^{m1 + m2,n1 + n2} :=
  concatTr (concatTc M11 M12) (concatTc M21 M22).

Definition insertTr {m n} (M : 'E^{m,n}) A i0 : 'E^{m.+1,n} := insertF M A i0.

Definition insertTc {m n} (M : 'E^{m,n}) B j0 : 'E^{m,n.+1} :=
  fun iinsertF (M i) (B i) j0.

Definition insertT {m n} (M : 'E^{m,n}) A B x i0 j0 : 'E^{m.+1,n.+1} :=
  insertTr (insertTc M B j0) (insertF A x j0) i0.

Definition skipTr {m n} (M : 'E^{m.+1,n}) i0 : 'E^{m,n} := skipF M i0.

Definition skipTc {m n} (M : 'E^{m,n.+1}) j0 : 'E^{m,n} :=
  fun iskipF (M i) j0.

Definition skipT {m n} (M : 'E^{m.+1,n.+1}) i0 j0 : 'E^{m,n} :=
  skipTr (skipTc M j0) i0.

Definition replaceTr {m n} (M : 'E^{m,n}) A i0 : 'E^{m,n} := replaceF M A i0.

Definition replaceTc {m n} (M : 'E^{m,n}) B j0 : 'E^{m,n} :=
  fun ireplaceF (M i) (B i) j0.

Definition replaceT {m n} (M : 'E^{m,n}) A B x i0 j0 : 'E^{m,n} :=
  replaceTr (replaceTc M B j0) (replaceF A x j0) i0.

Definition permutTr {m n} pi (M : 'E^{m,n}) : 'E^{m,n} := permutF pi M.
Definition permutTc {m n} pj (M : 'E^{m,n}) : 'E^{m,n} :=
  fun ipermutF pj (M i).
Definition permutT {m n} pi pj (M : 'E^{m,n}) : 'E^{m,n} :=
  permutTr pi (permutTc pj M).

Definition revTr {m n} (M : 'E^{m,n}) : 'E^{m,n} := revF M.
Definition revTc {m n} (M : 'E^{m,n}) : 'E^{m,n} := fun irevF (M i).
Definition revT {m n} (M : 'E^{m,n}) : 'E^{m,n} := revTr (revTc M).

Definition moveTr {m n} (M : 'E^{m.+1,n}) (i0 i1 : 'I_m.+1) : 'E^{m.+1,n} :=
  moveF M i0 i1.
Definition moveTc {m n} (M : 'E^{m,n.+1}) (j0 j1 : 'I_n.+1) : 'E^{m,n.+1} :=
  fun imoveF (M i) j0 j1.
Definition moveT
    {m n} (M : 'E^{m.+1,n.+1}) (i0 i1 : 'I_m.+1) (j0 j1 : 'I_n.+1) :
    'E^{m.+1,n.+1} :=
  moveTr (moveTc M j0 j1) i0 i1.

Definition transpTr {m n} (M : 'E^{m.+1,n}) (i0 i1 : 'I_m.+1) : 'E^{m.+1,n} :=
  transpF M i0 i1.
Definition transpTc {m n} (M : 'E^{m,n.+1}) (j0 j1 : 'I_n.+1) : 'E^{m,n.+1} :=
  fun itranspF (M i) j0 j1.
Definition transpT
    {m n} (M : 'E^{m.+1,n.+1}) (i0 i1 : 'I_m.+1) (j0 j1 : 'I_n.+1) :
    'E^{m.+1,n.+1} :=
  transpTr (transpTc M j0 j1) i0 i1.

Definition mapijT {m n} f (M : 'E^{m,n}) : 'F^{m,n} :=
  mapiF (fun imapiF (f i)) M.
Definition mapT {m n} f (M : 'E^{m,n}) : 'F^{m,n} := mapF (mapF f) M.

End FT_ops_Def1.

Section FT_ops_Facts0.

Correctness lemmas.

Context {E F : Type}.

Lemma constT_correct : m n (x : E), constT m n x = fun _ _x.
Proof. easy. Qed.

Lemma blk1T_00 : (x00 : E), blk1T x00 ord0 ord0 = x00.
Proof. easy. Qed.

Lemma blk1T_correct : (M : 'E^{1,1}), M = blk1T (M ord0 ord0).
Proof. intros; apply extT; move=>>; rewrite 2!I_1_is_unit; easy. Qed.

Lemma blk1T_equiv_def : (x00 : E), blk1T x00 = constT 1 1 x00.
Proof. easy. Qed.

Lemma blk2T_00 :
   (x00 x01 x10 x11 : E), blk2T x00 x01 x10 x11 ord0 ord0 = x00.
Proof. intros; unfold blk2T; rewrite 2!coupleF_0; easy. Qed.

Lemma blk2T_01 :
   (x00 x01 x10 x11 : E), blk2T x00 x01 x10 x11 ord0 ord_max = x01.
Proof. intros; unfold blk2T; rewrite coupleF_0 coupleF_1; easy. Qed.

Lemma blk2T_10 :
   (x00 x01 x10 x11 : E), blk2T x00 x01 x10 x11 ord_max ord0 = x10.
Proof. intros; unfold blk2T; rewrite coupleF_1 coupleF_0; easy. Qed.

Lemma blk2T_11 :
   (x00 x01 x10 x11 : E), blk2T x00 x01 x10 x11 ord_max ord_max = x11.
Proof. intros; unfold blk2T; rewrite 2!coupleF_1; easy. Qed.

Lemma blk2T_ul :
   (x00 x01 x10 x11 : E) (i j : 'I_2),
    i = ord0 j = ord0 blk2T x00 x01 x10 x11 i j = x00.
Proof. intros; subst; apply blk2T_00. Qed.

Lemma blk2T_ur :
   (x00 x01 x10 x11 : E) (i j : 'I_2),
    i = ord0 j = ord_max blk2T x00 x01 x10 x11 i j = x01.
Proof. intros; subst; apply blk2T_01. Qed.

Lemma blk2T_dl :
   (x00 x01 x10 x11 : E) (i j : 'I_2),
    i = ord_max j = ord0 blk2T x00 x01 x10 x11 i j = x10.
Proof. intros; subst; apply blk2T_10. Qed.

Lemma blk2T_dr :
   (x00 x01 x10 x11 : E) (i j : 'I_2),
    i = ord_max j = ord_max blk2T x00 x01 x10 x11 i j = x11.
Proof. intros; subst; apply blk2T_11. Qed.

Lemma blk2T_correct :
   (M : 'E^{2,2}),
    M = blk2T (M ord0 ord0) (M ord0 ord_max)
              (M ord_max ord0) (M ord_max ord_max).
Proof. intros; unfold blk2T; rewrite -3!coupleF_correct; easy. Qed.

Lemma row_correct : {m n} (M : 'E^{m,n}), row M = M.
Proof. easy. Qed.

Lemma col_correct : {m n} (M : 'E^{m,n}), col M = flipT M.
Proof. easy. Qed.

Lemma row_equiv_def : {m n} (M : 'E^{m,n}), row M = col (flipT M).
Proof. easy. Qed.

Lemma col_equiv_def : {m n} (M : 'E^{m,n}), col M = row (flipT M).
Proof. easy. Qed.

Lemma castT_equiv_def :
   {m1 m2 n1 n2} (Hm : m1 = m2) (Hn : n1 = n2) (M1 : 'E^{m1,n1}),
    castT Hm Hn M1 = castTc Hn (castTr Hm M1).
Proof. easy. Qed.

Lemma ulT_equiv_def :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}), ulT M = leftT (upT M).
Proof. easy. Qed.

Lemma urT_equiv_def :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}), urT M = rightT (upT M).
Proof. easy. Qed.

Lemma dlT_equiv_def :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}), dlT M = leftT (downT M).
Proof. easy. Qed.

Lemma drT_equiv_def :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}), drT M = rightT (downT M).
Proof. easy. Qed.

Lemma concatTr_correct_u :
   {m1 m2 n} (M1 : 'E^{m1,n}) (M2 : 'E^{m2,n})
      {i : 'I_(m1 + m2)} (Hi : (i < m1)%coq_nat),
    concatTr M1 M2 i = M1 (concat_l_ord Hi).
Proof. intros; apply concatF_correct_l. Qed.

Lemma concatTr_correct_d :
   {m1 m2 n} (M1 : 'E^{m1,n}) (M2 : 'E^{m2,n})
      {i : 'I_(m1 + m2)} (Hi : ¬ (i < m1)%coq_nat),
    concatTr M1 M2 i = M2 (concat_r_ord Hi).
Proof. intros; apply concatF_correct_r. Qed.

Lemma concatTc_correct_l :
   {m n1 n2} (M1 : 'E^{m,n1}) (M2 : 'E^{m,n2})
      i {j : 'I_(n1 + n2)} (Hj : (j < n1)%coq_nat),
    concatTc M1 M2 i j = M1 i (concat_l_ord Hj).
Proof. intros; apply concatF_correct_l. Qed.

Lemma concatTc_correct_r :
   {m n1 n2} (M1 : 'E^{m,n1}) (M2 : 'E^{m,n2})
      i {j : 'I_(n1 + n2)} (Hj : ¬ (j < n1)%coq_nat),
    concatTc M1 M2 i j = M2 i (concat_r_ord Hj).
Proof. intros; apply concatF_correct_r. Qed.

Lemma concatT_correct_ul :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2})
      {i : 'I_(m1 + m2)} {j : 'I_(n1 + n2)}
      (Hi : (i < m1)%coq_nat) (Hj : (j < n1)%coq_nat),
    concatT M11 M12 M21 M22 i j = M11 (concat_l_ord Hi) (concat_l_ord Hj).
Proof.
intros; unfold concatT; rewrite concatTr_correct_u concatTc_correct_l; easy.
Qed.

Lemma concatT_correct_ur :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2})
      {i : 'I_(m1 + m2)} {j : 'I_(n1 + n2)}
      (Hi : (i < m1)%coq_nat) (Hj : ¬ (j < n1)%coq_nat),
    concatT M11 M12 M21 M22 i j = M12 (concat_l_ord Hi) (concat_r_ord Hj).
Proof.
intros; unfold concatT; rewrite concatTr_correct_u concatTc_correct_r; easy.
Qed.

Lemma concatT_correct_dl :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2})
      {i : 'I_(m1 + m2)} {j : 'I_(n1 + n2)}
      (Hi : ¬ (i < m1)%coq_nat) (Hj : (j < n1)%coq_nat),
    concatT M11 M12 M21 M22 i j = M21 (concat_r_ord Hi) (concat_l_ord Hj).
Proof.
intros; unfold concatT; rewrite concatTr_correct_d concatTc_correct_l; easy.
Qed.

Lemma concatT_correct_dr :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2})
      {i : 'I_(m1 + m2)} {j : 'I_(n1 + n2)}
      (Hi : ¬ (i < m1)%coq_nat) (Hj : ¬ (j < n1)%coq_nat),
    concatT M11 M12 M21 M22 i j = M22 (concat_r_ord Hi) (concat_r_ord Hj).
Proof.
intros; unfold concatT; rewrite concatTr_correct_d concatTc_correct_r; easy.
Qed.

Lemma concatT_equiv_def :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}),
    concatT M11 M12 M21 M22 = concatTc (concatTr M11 M21) (concatTr M12 M22).
Proof.
intros; apply extT; intros i j; unfold concatT.
destruct (lt_dec i m1) as [Hi | Hi], (lt_dec j n1) as [Hj | Hj].
do 2 rewrite concatTc_correct_l concatTr_correct_u; easy.
do 2 rewrite concatTc_correct_r concatTr_correct_u; easy.
do 2 rewrite concatTc_correct_l concatTr_correct_d; easy.
do 2 rewrite concatTc_correct_r concatTr_correct_d; easy.
Qed.

Lemma widenT_S_equiv_def :
   {m n} (M : 'E^{m.+1,n.+1}), widenT_S M = widenTc_S (widenTr_S M).
Proof. easy. Qed.

Lemma liftT_S_equiv_def :
   {m n} (M : 'E^{m.+1,n.+1}), liftT_S M = liftTc_S (liftTr_S M).
Proof. easy. Qed.

Lemma insertTr_correct_l :
   {m n} (M : 'E^{m,n}) A {i0 i}, i = i0 insertTr M A i0 i = A.
Proof. intros; apply insertF_correct_l; easy. Qed.

Lemma insertTr_correct_r :
   {m n} (M : 'E^{m,n}) A {i0 i} (H : i i0),
    insertTr M A i0 i = M (insert_ord H).
Proof. intros; apply insertF_correct_r; easy. Qed.

Lemma insertTc_correct_l :
   {m n} (M : 'E^{m,n}) B {j0} i {j},
    j = j0 insertTc M B j0 i j = B i.
Proof. intros; apply insertF_correct_l; easy. Qed.

Lemma insertTc_correct_r :
   {m n} (M : 'E^{m,n}) B {j0} i {j} (H : j j0),
    insertTc M B j0 i j = M i (insert_ord H).
Proof. intros; apply insertF_correct_r; easy. Qed.

Lemma insertT_correct_lr :
   {m n} (M : 'E^{m,n}) A B x {i0} j0 {i},
    i = i0 insertT M A B x i0 j0 i = insertF A x j0.
Proof. move=>>; apply insertTr_correct_l. Qed.

Lemma insertT_correct_lc :
   {m n} (M : 'E^{m,n}) A B x i0 {j0} i {j},
    j = j0 insertT M A B x i0 j0 i j = insertF B x i0 i.
Proof.
intros m n M A B x i0 j0 i j Hj; unfold insertT.
destruct (ord_eq_dec i i0) as [Hi | Hi].
rewriteinsertTr_correct_l, 2!insertF_correct_l; easy.
rewrite insertTr_correct_r insertF_correct_r insertTc_correct_l; easy.
Qed.

Lemma insertT_correct_r :
   {m n} (M : 'E^{m,n}) A B x {i0 j0 i j} (Hi : i i0) (Hj : j j0),
    insertT M A B x i0 j0 i j = M (insert_ord Hi) (insert_ord Hj).
Proof.
intros; unfold insertT; rewrite insertTr_correct_r insertTc_correct_r; easy.
Qed.

Lemma insertT_equiv_def :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    insertT M A B x i0 j0 = insertTc (insertTr M A i0) (insertF B x i0) j0.
Proof.
intros m n M A B x i0 j0; apply extT; intros i j.
destruct (ord_eq_dec i i0) as [Hi | Hi], (ord_eq_dec j j0) as [Hj | Hj].
rewriteinsertT_correct_lr, insertTc_correct_l, 2!insertF_correct_l; easy.
rewriteinsertT_correct_lr, (insertTc_correct_r _ _ _ Hj),
    (insertF_correct_r _ _ Hj), insertTr_correct_l; easy.
rewriteinsertT_correct_lc, insertTc_correct_l; easy.
rewrite → (insertT_correct_r _ _ _ _ Hi Hj), (insertTc_correct_r _ _ _ Hj),
    (insertTr_correct_r _ _ Hi); easy.
Qed.

Lemma skipTr_correct_l :
   {m n} (M : 'E^{m.+1,n}) (i0 : 'I_m.+1) (i : 'I_m),
    (i < i0)%coq_nat skipTr M i0 i = widenTr_S M i.
Proof. move=>>; apply skipF_correct_l. Qed.

Lemma skipTr_correct_r :
   {m n} (M : 'E^{m.+1,n}) (i0 : 'I_m.+1) (i : 'I_m),
    ¬ (i < i0)%coq_nat skipTr M i0 i = liftTr_S M i.
Proof. move=>>; apply skipF_correct_r. Qed.

Lemma skipTr_correct :
   {m n} (M : 'E^{m.+1,n}) i0 i j, skipTr M i0 i j = M (skip_ord i0 i) j.
Proof. easy. Qed.

Lemma skipTc_correct_l :
   {m n} (M : 'E^{m,n.+1}) (j0 : 'I_n.+1) i (j : 'I_n),
    (j < j0)%coq_nat skipTc M j0 i j = widenTc_S M i j.
Proof. move=>>; apply skipF_correct_l. Qed.

Lemma skipTc_correct_r :
   {m n} (M : 'E^{m,n.+1}) (j0 : 'I_n.+1) i (j : 'I_n),
    ¬ (j < j0)%coq_nat skipTc M j0 i j = liftTc_S M i j.
Proof. move=>>; apply skipF_correct_r. Qed.

Lemma skipTc_correct :
   {m n} (M : 'E^{m,n.+1}) j0 i j, skipTc M j0 i j = M i (skip_ord j0 j).
Proof. easy. Qed.

Lemma skipT_correct_ll :
   {m n} (M : 'E^{m.+1,n.+1})
      (i0 : 'I_m.+1) (j0 : 'I_n.+1) (i : 'I_m) (j : 'I_n),
    (i < i0)%coq_nat (j < j0)%coq_nat skipT M i0 j0 i j = widenT_S M i j.
Proof.
intros; unfold skipT.
rewrite skipTr_correct_l; try apply skipTc_correct_l; easy.
Qed.

Lemma skipT_correct_lr :
   {m n} (M : 'E^{m.+1,n.+1})
      (i0 : 'I_m.+1) (j0 : 'I_n.+1) (i : 'I_m) (j : 'I_n),
    (i < i0)%coq_nat ¬ (j < j0)%coq_nat
    skipT M i0 j0 i j = widenTr_S (liftTc_S M) i j.
Proof.
intros; unfold skipT.
rewrite skipTr_correct_l; try apply skipTc_correct_r; easy.
Qed.

Lemma skipT_correct_rl :
   {m n} (M : 'E^{m.+1,n.+1})
      (i0 : 'I_m.+1) (j0 : 'I_n.+1) (i : 'I_m) (j : 'I_n),
    ¬ (i < i0)%coq_nat (j < j0)%coq_nat
    skipT M i0 j0 i j = liftTr_S (widenTc_S M) i j.
Proof.
intros; unfold skipT.
rewrite skipTr_correct_r; try apply skipTc_correct_l; easy.
Qed.

Lemma skipT_correct_rr :
   {m n} (M : 'E^{m.+1,n.+1})
      (i0 : 'I_m.+1) (j0 : 'I_n.+1) (i : 'I_m) (j : 'I_n),
    ¬ (i < i0)%coq_nat ¬ (j < j0)%coq_nat
    skipT M i0 j0 i j = liftT_S M i j.
Proof.
intros; unfold skipT.
rewrite skipTr_correct_r; try apply skipTc_correct_r; easy.
Qed.

Lemma skipT_correct :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0 i j,
    skipT M i0 j0 i j = M (skip_ord i0 i) (skip_ord j0 j).
Proof. easy. Qed.

Lemma flipT_skipT_correct :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0,
    flipT (skipT M i0 j0) = skipF (fun j(skipF M i0)^~ j) j0.
Proof. easy. Qed.

Lemma skipT_equiv_def :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0, skipT M i0 j0 = skipTc (skipTr M i0) j0.
Proof. easy. Qed.

Lemma replaceTr_correct_l :
   {m n} (M : 'E^{m,n}) A {i0 i}, i = i0 replaceTr M A i0 i = A.
Proof. move=>>; apply replaceF_correct_l. Qed.

Lemma replaceTr_correct_r :
   {m n} (M : 'E^{m,n}) A {i0 i}, i i0 replaceTr M A i0 i = M i.
Proof. move=>>; apply replaceF_correct_r. Qed.

Lemma replaceTc_correct_l :
   {m n} (M : 'E^{m,n}) B {j0} i {j},
    j = j0 replaceTc M B j0 i j = B i.
Proof. move=>>; apply replaceF_correct_l. Qed.

Lemma replaceTc_correct_r :
   {m n} (M : 'E^{m,n}) B {j0} i {j},
    j j0 replaceTc M B j0 i j = M i j.
Proof. move=>>; apply replaceF_correct_r. Qed.

Lemma replaceT_correct_lr :
   {m n} (M : 'E^{m,n}) A B x {i0} j0 {i},
    i = i0 replaceT M A B x i0 j0 i = replaceF A x j0.
Proof. move=>>; apply replaceTr_correct_l. Qed.

Lemma replaceT_correct_lc :
   {m n} (M : 'E^{m,n}) A B x i0 {j0} i {j},
    j = j0 replaceT M A B x i0 j0 i j = replaceF B x i0 i.
Proof.
intros m n M A B x i0 j0 i j Hj; unfold replaceT.
destruct (ord_eq_dec i i0) as [Hi | Hi].
rewritereplaceTr_correct_l, 2!replaceF_correct_l; easy.
rewritereplaceTr_correct_r, replaceF_correct_r, replaceTc_correct_l; easy.
Qed.

Lemma replaceT_correct_r :
   {m n} (M : 'E^{m,n}) A B x {i0 j0 i j},
    i i0 j j0 replaceT M A B x i0 j0 i j = M i j.
Proof.
intros; unfold replaceT;
    rewritereplaceTr_correct_r, replaceTc_correct_r; easy.
Qed.

Lemma replaceT_equiv_def :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    replaceT M A B x i0 j0 = replaceTc (replaceTr M A i0) (replaceF B x i0) j0.
Proof.
intros; apply extT; intros i j.
destruct (ord_eq_dec i i0) as [Hi | Hi], (ord_eq_dec j j0) as [Hj | Hj].
rewritereplaceT_correct_lc, replaceTc_correct_l; easy.
rewritereplaceT_correct_lr, replaceTc_correct_r,
    replaceF_correct_r, replaceTr_correct_l; easy.
rewritereplaceT_correct_lc, replaceTc_correct_l, replaceF_correct_r; easy.
rewritereplaceT_correct_r, replaceTc_correct_r, replaceTr_correct_r; easy.
Qed.

Lemma mapijT_correct :
   {m n} (f : '(E F)^{m,n}) (M : 'E^{m,n}),
    mapijT f M = fun i jf i j (M i j).
Proof. easy. Qed.

Lemma mapT_correct :
   {m n} (f : E F) (M : 'E^{m,n}), mapT f M = fun i jf (M i j).
Proof. easy. Qed.

Lemma mapT_equiv_def :
   {m n} (f : E F) (M : 'E^{m,n}), mapT f M = mapijT (fun _ _f) M.
Proof. easy. Qed.

End FT_ops_Facts0.

Section FT_ops_Facts1.

Lemma hat0nT_is_nonempty : (E : Type) n, inhabited 'E^{0,n}.
Proof. intros; apply hat0F_is_nonempty. Qed.

Lemma hatm0T_is_nonempty : (E : Type) m, inhabited 'E^{m,0}.
Proof. intros; apply fun_to_nonempty_compat, hat0F_is_nonempty. Qed.

Context {E : Type}.

Lemma hat0nT_unit : n (N : 'E^{0,n}), unit_type N.
Proof. intros; apply hat0F_unit. Qed.

Lemma hat0nT_is_unit : n, is_unit_type 'E^{0,n}.
Proof. intros; apply hat0F_is_unit. Qed.

Lemma hatm0T_is_unit : m, is_unit_type 'E^{m,0}.
Proof. intros; apply fun_to_is_unit_is_unit, hat0F_is_unit. Qed.

Lemma hatm0T_unit : m (M : 'E^{m,0}), unit_type M.
Proof. intros; apply unit_type_correct, hatm0T_is_unit. Qed.

Properties of constructors constT/blk1T/blk2T.

Lemma constT_eq :
   {m n} (x y : E), x = y constT m n x = constT m n y.
Proof. intros; f_equal; easy. Qed.

Lemma blk1T_eq :
   (x00 y00 : E), x00 = y00 blk1T x00 = blk1T y00.
Proof. intros; f_equal; easy. Qed.

Lemma blk2T_eq :
   (x00 x01 x10 x11 y00 y01 y10 y11 : E),
    x00 = y00 x01 = y01 x10 = y10 x11 = y11
    blk2T x00 x01 x10 x11 = blk2T y00 y01 y10 y11.
Proof. intros; f_equal; easy. Qed.

Lemma constT_inj :
   m n (x1 x2 : E), constT m.+1 n.+1 x1 = constT m.+1 n.+1 x2 x1 = x2.
Proof. intros; apply (constF_inj n), (constF_inj m); easy. Qed.

Lemma blk1T_inj :
   (x00 y00 : E), blk1T x00 = blk1T y00 x00 = y00.
Proof. intros; apply (constT_inj 0 0); easy. Qed.

Lemma blk2T_inj_00 :
   (x00 x01 x10 x11 y00 y01 y10 y11 : E),
    blk2T x00 x01 x10 x11 = blk2T y00 y01 y10 y11 x00 = y00.
Proof.
intros x00 x01 x10 x11 y00 y01 y10 y11 H.
erewrite <- (blk2T_00 x00 x01 x10 x11), <- (blk2T_00 y00 y01 y10 y11), H; easy.
Qed.

Lemma blk2T_inj_01 :
   (x00 x01 x10 x11 y00 y01 y10 y11 : E),
    blk2T x00 x01 x10 x11 = blk2T y00 y01 y10 y11 x01 = y01.
Proof.
intros x00 x01 x10 x11 y00 y01 y10 y11 H.
erewrite <- (blk2T_01 x00 x01 x10 x11), <- (blk2T_01 y00 y01 y10 y11), H; easy.
Qed.

Lemma blk2T_inj_10 :
   (x00 x01 x10 x11 y00 y01 y10 y11 : E),
    blk2T x00 x01 x10 x11 = blk2T y00 y01 y10 y11 x10 = y10.
Proof.
intros x00 x01 x10 x11 y00 y01 y10 y11 H.
erewrite <- (blk2T_10 x00 x01 x10 x11), <- (blk2T_10 y00 y01 y10 y11), H; easy.
Qed.

Lemma blk2T_inj_11 :
   (x00 x01 x10 x11 y00 y01 y10 y11 : E),
    blk2T x00 x01 x10 x11 = blk2T y00 y01 y10 y11 x11 = y11.
Proof.
intros x00 x01 x10 x11 y00 y01 y10 y11 H.
erewrite <- (blk2T_11 x00 x01 x10 x11), <- (blk2T_11 y00 y01 y10 y11), H; easy.
Qed.

Lemma blk2T_inj :
   (x00 x01 x10 x11 y00 y01 y10 y11 : E),
    blk2T x00 x01 x10 x11 = blk2T y00 y01 y10 y11
    x00 = y00 x01 = y01 x10 = y10 x11 = y11.
Proof.
move=>> H; repeat split;
    [eapply blk2T_inj_00 | eapply blk2T_inj_01 |
     eapply blk2T_inj_10 | eapply blk2T_inj_11]; apply H.
Qed.

Properties of destructors row/col.
Properties of predicates eqxTr/eqxTc/eqxT.

Lemma eqxTr_refl : {m n} (M : 'E^{m,n}) i0, eqxTr M M i0.
Proof. easy. Qed.

Lemma eqxTr_sym :
   {m n} (M N : 'E^{m,n}) i0, eqxTr M N i0 eqxTr N M i0.
Proof. move=>>; apply eqxF_sym. Qed.

Lemma eqxTr_trans :
   {m n} (M N P : 'E^{m,n}) i0,
    eqxTr M N i0 eqxTr N P i0 eqxTr M P i0.
Proof. move=>>; apply eqxF_trans. Qed.

Lemma eqxTc_refl : {m n} (M : 'E^{m,n}) j0, eqxTc M M j0.
Proof. easy. Qed.

Lemma eqxTc_sym :
   {m n} (M N : 'E^{m,n}) j0, eqxTc M N j0 eqxTc N M j0.
Proof. move=>> H i; apply eqxF_sym; easy. Qed.

Lemma eqxTc_trans :
   {m n} (M N P : 'E^{m,n}) j0,
    eqxTc M N j0 eqxTc N P j0 eqxTc M P j0.
Proof. move=>> H1 H2 i; eapply eqxF_trans; [apply H1 | apply H2]. Qed.

Lemma eqxT_refl : {m n} (M : 'E^{m,n}) i0 j0, eqxT M M i0 j0.
Proof. easy. Qed.

Lemma eqxT_sym :
   {m n} (M N : 'E^{m,n}) i0 j0, eqxT M N i0 j0 eqxT N M i0 j0.
Proof. move=>> H i j Hi Hj; symmetry; apply (H _ _ Hi Hj). Qed.

Lemma eqxT_trans :
   {m n} (M N P : 'E^{m,n}) i0 j0,
    eqxT M N i0 j0 eqxT N P i0 j0 eqxT M P i0 j0.
Proof. move=>> H1 H2 i j Hi Hj; rewrite H1; auto. Qed.

Lemma eqxTr_compat : {m n} (M N : 'E^{m,n}) i0, M = N eqxTr M N i0.
Proof. move=>>; apply eqxF_compat. Qed.

Lemma eqxTc_compat : {m n} (M N : 'E^{m,n}) j0, M = N eqxTc M N j0.
Proof. move=>> H; rewrite H; easy. Qed.

Lemma eqxT_compat :
   {m n} (M N : 'E^{m,n}) i0 j0, M = N eqxT M N i0 j0.
Proof. move=>> H; rewrite H; easy. Qed.

Lemma eqxTr_reg :
   {m n} (M N : 'E^{m,n}) i0,
    row M i0 = row N i0 eqxTr M N i0 M = N.
Proof. move=>>; apply eqxF_reg. Qed.

Lemma eqxTc_reg :
   {m n} (M N : 'E^{m,n}) j0,
    col M j0 = col N j0 eqxTc M N j0 M = N.
Proof.
movem n M N j0 /extF_rev H0 H1; apply extT; intros i j; specialize (H0 i).
destruct (ord_eq_dec j j0) as [Hj |]; [rewrite Hj | apply H1]; easy.
Qed.

Lemma eqxT_reg :
   {m n} (M N : 'E^{m,n}) i0 j0,
    row M i0 = row N i0 col M j0 = col N j0 eqxT M N i0 j0 M = N.
Proof.
movem n M N i0 j0 /extF_rev Hr0 /extF_rev Hc0 H1;
    apply extT; intros i j; specialize (Hr0 j); specialize (Hc0 i).
destruct (ord_eq_dec i i0) as [Hi |], (ord_eq_dec j j0) as [Hj |];
    try rewrite Hi; try rewrite Hj; auto; rewrite -Hj; easy.
Qed.

Lemma eqxTr_not_equiv :
   {m n} (M N : 'E^{m,n}) i0, eqxTr M N i0 ¬ neqxTr M N i0.
Proof. intros; apply eqxF_not_equiv. Qed.

Lemma neqxTr_not_equiv :
   {m n} (M N : 'E^{m,n}) i0, neqxTr M N i0 ¬ eqxTr M N i0.
Proof. intros; apply neqxF_not_equiv. Qed.

Lemma eqxTc_not_equiv :
   {m n} (M N : 'E^{m,n}) j0, eqxTc M N j0 ¬ neqxTc M N j0.
Proof.
intros; split.
intros H; apply all_not_not_ex; intros; apply eqxF_not_equiv, H.
move⇒ /not_ex_all_not H i; apply eqxF_not_equiv, H.
Qed.

Lemma neqxTc_not_equiv :
   {m n} (M N : 'E^{m,n}) j0, neqxTc M N j0 ¬ eqxTc M N j0.
Proof. intros; rewrite iff_not_r_equiv eqxTc_not_equiv; easy. Qed.

Lemma eqxT_not_equiv :
   {m n} (M N : 'E^{m,n}) i0 j0, eqxT M N i0 j0 ¬ neqxT M N i0 j0.
Proof.
intros; split.
intros H; do 2 (apply all_not_not_ex; intros); apply imp3_and_equiv, H.
move⇒ /not_ex_all_not H i j; apply imp3_and_equiv; apply (not_ex_all_not _ _ (H i)).
Qed.

Lemma neqxT_not_equiv :
   {m n} (M N : 'E^{m,n}) i0 j0, neqxT M N i0 j0 ¬ eqxT M N i0 j0.
Proof. intros; rewrite iff_not_r_equiv eqxT_not_equiv; easy. Qed.

Lemma neqxTr_compat :
   {m n} (M N : 'E^{m,n}) i0,
    M N row M i0 row N i0 neqxTr M N i0.
Proof. move=>>; apply neqxF_compat. Qed.

Lemma neqxTc_compat :
   {m n} (M N : 'E^{m,n}) j0,
    M N col M j0 col N j0 neqxTc M N j0.
Proof.
move=>>; rewrite neqxTc_not_equiv -not_and_equiv -contra_equiv.
intros [H1 H2]; apply (eqxTc_reg _ _ _ H1 H2).
Qed.

Lemma neqxT_compat :
   {m n} (M N : 'E^{m,n}) i0 j0,
    M N row M i0 row N i0 col M j0 col N j0 neqxT M N i0 j0.
Proof.
move=>>; rewrite neqxT_not_equiv -not_and3_equiv -contra_equiv.
intros [H1 [H2 H3]]; apply (eqxT_reg _ _ _ _ H1 H2 H3).
Qed.

Lemma neqxTr_reg : {m n} (M N : 'E^{m,n}) i0, neqxTr M N i0 M N.
Proof. move=>>; apply neqxF_reg. Qed.

Lemma neqxTc_reg : {m n} (M N : 'E^{m,n}) j0, neqxTc M N j0 M N.
Proof. move=>>; rewrite neqxTc_not_equiv -contra_equiv; apply eqxTc_compat. Qed.

Lemma neqxT_reg :
   {m n} (M N : 'E^{m,n}) i0 j0, neqxT M N i0 j0 M N.
Proof. move=>>; rewrite neqxT_not_equiv -contra_equiv; apply eqxT_compat. Qed.

Properties of operators castTr/castTc/castT.

Lemma castTr_refl : {m n} {Hm : m = m} (M : 'E^{m,n}), castTr Hm M = M.
Proof. intros; apply castF_refl. Qed.

Lemma castTc_refl : {m n} {Hn : n = n} (M : 'E^{m,n}), castTc Hn M = M.
Proof. intros; apply extF; intro; apply castF_refl. Qed.

Lemma castT_refl :
   {m n} {Hm : m = m} {Hn : n = n} (M : 'E^{m,n}), castT Hm Hn M = M.
Proof. intros; unfold castT; rewrite castTc_refl castTr_refl; easy. Qed.

Lemma castTr_id : {m n} {Hm : m = m}, castTr Hm = @id 'E^{m,n}.
Proof. intros; apply castF_id. Qed.

Lemma castTc_id : {m n} {Hn : n = n}, castTc Hn = @id 'E^{m,n}.
Proof. intros; apply fun_ext; intro; apply castTc_refl. Qed.

Lemma castT_id :
   {m n} {Hm : m = m} {Hn : n = n}, castT Hm Hn = @id 'E^{m,n}.
Proof. intros; unfold castT; rewrite castTc_id castTr_id; easy. Qed.

Lemma castTr_comp :
   {m1 m2 m3 n} (Hm12 : m1 = m2) (Hm23 : m2 = m3) (M1 : 'E^{m1,n}),
    castTr Hm23 (castTr Hm12 M1) = castTr (eq_trans Hm12 Hm23) M1.
Proof. intros; apply castF_comp. Qed.

Lemma castTc_comp :
   {m n1 n2 n3} (Hn12 : n1 = n2) (Hn23 : n2 = n3) (M1 : 'E^{m,n1}),
    castTc Hn23 (castTc Hn12 M1) = castTc (eq_trans Hn12 Hn23) M1.
Proof. intros; apply extF; intro; apply castF_comp. Qed.

Lemma castT_comp :
   {m1 m2 m3 n1 n2 n3} (Hm12 : m1 = m2) (Hm23 : m2 = m3)
      (Hn12 : n1 = n2) (Hn23 : n2 = n3) (M1 : 'E^{m1,n1}),
    castT Hm23 Hn23 (castT Hm12 Hn12 M1) =
      castT (eq_trans Hm12 Hm23) (eq_trans Hn12 Hn23) M1.
Proof.
intros; unfold castT; rewrite -castT_equiv_def; unfold castT.
rewrite castTr_comp castTc_comp; easy.
Qed.

Lemma castT_comp_rl :
   {m1 m2 m3 n1 n2}
      (Hm12 : m1 = m2) (Hm23 : m2 = m3) (Hn : n1 = n2) (M1 : 'E^{m1,n1}),
    castTr Hm23 (castT Hm12 Hn M1) = castT (eq_trans Hm12 Hm23) Hn M1.
Proof. intros; unfold castT; rewrite castTr_comp; easy. Qed.

Lemma castT_comp_rr :
   {m1 m2 m3 n1 n2}
      (Hm12 : m1 = m2) (Hm23 : m2 = m3) (Hn : n1 = n2) (M1 : 'E^{m1,n1}),
    castT Hm23 Hn (castTr Hm12 M1) = castT (eq_trans Hm12 Hm23) Hn M1.
Proof.
intros; unfold castT; rewrite -castT_equiv_def; unfold castT.
rewrite castTr_comp; easy.
Qed.

Lemma castT_comp_cl :
   {m1 m2 n1 n2 n3}
      (Hm : m1 = m2) (Hn12 : n1 = n2) (Hn23 : n2 = n3) (M1 : 'E^{m1,n1}),
    castTc Hn23 (castT Hm Hn12 M1) = castT Hm (eq_trans Hn12 Hn23) M1.
Proof.
intros; unfold castT; rewrite -castT_equiv_def; unfold castT.
rewrite castTc_comp; easy.
Qed.

Lemma castT_comp_cr :
   {m1 m2 n1 n2 n3}
      (Hm : m1 = m2) (Hn12 : n1 = n2) (Hn23 : n2 = n3) (M1 : 'E^{m1,n1}),
    castT Hm Hn23 (castTc Hn12 M1) = castT Hm (eq_trans Hn12 Hn23) M1.
Proof. intros; unfold castT; rewrite castTc_comp; easy. Qed.

Lemma castTr_can :
   {m1 m2 n} (Hm12 : m1 = m2) (Hm21 : m2 = m1),
    cancel (@castTr E _ _ n Hm12) (castTr Hm21).
Proof. intros; apply castF_can. Qed.

Lemma castTc_can :
   {m n1 n2} (Hn12 : n1 = n2) (Hn21 : n2 = n1),
    cancel (@castTc E m _ _ Hn12) (castTc Hn21).
Proof. move=>>; apply extF; intro; apply castF_can. Qed.

Lemma castT_can :
   {m1 m2 n1 n2} (Hm12 : m1 = m2) (Hn12 : n1 = n2)
      (Hm21 : m2 = m1) (Hn21 : n2 = n1),
    cancel (@castT E _ _ _ _ Hm12 Hn12) (castT Hm21 Hn21).
Proof.
move=>>; unfold castT; rewrite -castT_equiv_def; unfold castT.
rewrite castTr_can castTc_can; easy.
Qed.

Lemma castTr_eq :
   {m1 m2 n} (Hm : m1 = m2) (M1 N1 : 'E^{m1,n}),
    M1 = N1 castTr Hm M1 = castTr Hm N1.
Proof. intros; f_equal; easy. Qed.

Lemma castTc_eq :
   {m n1 n2} (Hn : n1 = n2) (M1 N1 : 'E^{m,n1}),
    M1 = N1 castTc Hn M1 = castTc Hn N1.
Proof. intros; f_equal; easy. Qed.

Lemma castT_eq :
   {m1 m2 n1 n2} (Hm : m1 = m2) (Hn : n1 = n2) (M1 N1 : 'E^{m1,n1}),
    M1 = N1 castT Hm Hn M1 = castT Hm Hn N1.
Proof. intros; f_equal; easy. Qed.

Lemma castTr_inj :
   {m1 m2 n} (Hm : m1 = m2) (M1 N1 : 'E^{m1,n}),
    castTr Hm M1 = castTr Hm N1 M1 = N1.
Proof. intros m1 m2 n Hm M1 N1; apply castF_inj. Qed.

Lemma castTc_inj :
   {m n1 n2} (Hn : n1 = n2) (M1 N1 : 'E^{m,n1}),
    castTc Hn M1 = castTc Hn N1 M1 = N1.
Proof.
intros m n1 n2 Hn M1 N1 H; apply extF; intro.
apply (castF_inj Hn), (extF_rev _ _ H i).
Qed.

Lemma castT_inj :
   {m1 m2 n1 n2} (Hm : m1 = m2) (Hn : n1 = n2) (M1 N1 : 'E^{m1,n1}),
    castT Hm Hn M1 = castT Hm Hn N1 M1 = N1.
Proof.
intros m1 m2 n1 n2 Hm Hn M1 N1; move⇒ /castTr_inj /castTc_inj; easy.
Qed.

Properties of operator flipT.

Lemma flipT_invol : {n1 n2} (M : 'E^{n1,n2}), flipT (flipT M) = M.
Proof. easy. Qed.

Lemma flipT_eq : {m n} (M N : 'E^{m,n}), M = N flipT M = flipT N.
Proof. intros; f_equal; easy. Qed.

Lemma flipT_inj : {m n} (M N : 'E^{m,n}), flipT M = flipT N M = N.
Proof.
intros m n M N; rewrite -{2}(flipT_invol M) -{2}(flipT_invol N).
apply flipT_eq.
Qed.

Lemma eqxTr_flipT :
   {m n} (M N : 'E^{m,n}) j0,
    eqxTr (flipT M) (flipT N) j0 eqxTc M N j0.
Proof.
intros m n M N j0; split; intros H.
intros i j Hj; specialize (H j Hj); apply (extF_rev _ _ H i).
intros j Hj; apply extF; intros i; apply (H i j Hj).
Qed.

Lemma eqxTc_flipT :
   {m n} (M N : 'E^{m,n}) i0,
    eqxTc (flipT M) (flipT N) i0 eqxTr M N i0.
Proof. intros; rewrite eqxTr_flipT; easy. Qed.

Lemma flipT_castTr :
   {m1 m2 n} (Hm : m1 = m2) (M : 'E^{m1,n}),
    flipT (castTr Hm M) = castTc Hm (flipT M).
Proof. easy. Qed.

Lemma flipT_castTc :
   {m n1 n2} (Hn : n1 = n2) (M : 'E^{m,n1}),
    flipT (castTc Hn M) = castTr Hn (flipT M).
Proof. easy. Qed.

Lemma flipT_castT :
   {m1 m2 n1 n2} (Hm : m1 = m2) (Hn : n1 = n2) (M : 'E^{m1,n1}),
    flipT (castT Hm Hn M) = castT Hn Hm (flipT M).
Proof. easy. Qed.

Properties of operators upT/downT/leftT/rightT/ulT/urT/dlT/drT.

Lemma upT_compat :
   {m1 m2 n} (M N : 'E^{m1 + m2,n}),
    ( i : 'I_(m1 + m2), (i < m1)%coq_nat M i = N i)
    upT M = upT N.
Proof. intros; apply firstF_compat; easy. Qed.

Lemma downT_compat :
   {m1 m2 n} (M N : 'E^{m1 + m2,n}),
    ( i : 'I_(m1 + m2), (m1 i)%coq_nat M i = N i)
    downT M = downT N.
Proof. intros; apply lastF_compat; easy. Qed.

Lemma leftT_compat :
   {m n1 n2} (M N : 'E^{m,n1 + n2}),
    ( i (j : 'I_(n1 + n2)), (j < n1)%coq_nat M i j = N i j)
    leftT M = leftT N.
Proof. intros; apply extF; intro; apply firstF_compat; auto. Qed.

Lemma rightT_compat :
   {m n1 n2} (M N : 'E^{m,n1 + n2}),
    ( i (j : 'I_(n1 + n2)), (n1 j)%coq_nat M i j = N i j)
    rightT M = rightT N.
Proof. intros; apply extF; intro; apply lastF_compat; auto. Qed.

Lemma ulT_compat :
   {m1 m2 n1 n2} (M N : 'E^{m1 + m2,n1 + n2}),
    ( (i : 'I_(m1 + m2)) (j : 'I_(n1 + n2)),
      (i < m1)%coq_nat (j < n1)%coq_nat M i j = N i j)
    ulT M = ulT N.
Proof. intros; apply upT_compat; intros; apply firstF_compat; auto. Qed.

Lemma urT_compat :
   {m1 m2 n1 n2} (M N : 'E^{m1 + m2,n1 + n2}),
    ( (i : 'I_(m1 + m2)) (j : 'I_(n1 + n2)),
      (i < m1)%coq_nat (n1 j)%coq_nat M i j = N i j)
    urT M = urT N.
Proof. intros; apply upT_compat; intros; apply lastF_compat; auto. Qed.

Lemma dlT_compat :
   {m1 m2 n1 n2} (M N : 'E^{m1 + m2,n1 + n2}),
    ( (i : 'I_(m1 + m2)) (j : 'I_(n1 + n2)),
      (m1 i)%coq_nat (j < n1)%coq_nat M i j = N i j)
    dlT M = dlT N.
Proof. intros; apply downT_compat; intros; apply firstF_compat; auto. Qed.

Lemma drT_compat :
   {m1 m2 n1 n2} (M N : 'E^{m1 + m2,n1 + n2}),
    ( (i : 'I_(m1 + m2)) (j : 'I_(n1 + n2)),
      (m1 i)%coq_nat (n1 j)%coq_nat M i j = N i j)
    drT M = drT N.
Proof. intros; apply downT_compat; intros; apply lastF_compat; auto. Qed.

Lemma upT_castTc :
   {m1 m2 n1 n2} (Hn : n1 = n2) (M : 'E^{m1 + m2,n1}),
    upT (castTc Hn M) = castTc Hn (upT M).
Proof. easy. Qed.

Lemma downT_castTc :
   {m1 m2 n1 n2} (Hn : n1 = n2) (M : 'E^{m1 + m2,n1}),
    downT (castTc Hn M) = castTc Hn (downT M).
Proof. easy. Qed.

Lemma leftT_castTr :
   {m1 m2 n1 n2} (Hm : m1 = m2) (M : 'E^{m1, n1 + n2}),
    leftT (castTr Hm M) = castTr Hm (leftT M).
Proof. easy. Qed.

Lemma rightT_castTr :
   {m1 m2 n1 n2} (Hm : m1 = m2) (M : 'E^{m1, n1 + n2}),
    rightT (castTr Hm M) = castTr Hm (rightT M).
Proof. easy. Qed.

Lemma upT_leftT :
   {m m1 m2 n n1 n2} (Hm : m = m1 + m2) (Hn : n = n1 + n2)
      (M : 'E^{m,n}),
    upT (castTr Hm (leftT (castTc Hn M))) =
      leftT ( castTc Hn (upT (castTr Hm M))).
Proof. easy. Qed.

Lemma upT_rightT :
   {m m1 m2 n n1 n2} (Hm : m = m1 + m2) (Hn : n = n1 + n2)
      (M : 'E^{m,n}),
    upT (castTr Hm (rightT (castTc Hn M))) =
      rightT ( castTc Hn (upT (castTr Hm M))).
Proof. easy. Qed.

Lemma downT_leftT :
   {m m1 m2 n n1 n2} (Hm : m = m1 + m2) (Hn : n = n1 + n2)
      (M : 'E^{m,n}),
    downT (castTr Hm (leftT (castTc Hn M))) =
      leftT ( castTc Hn (downT (castTr Hm M))).
Proof. easy. Qed.

Lemma downT_rightT :
   {m m1 m2 n n1 n2} (Hm : m = m1 + m2) (Hn : n = n1 + n2)
      (M : 'E^{m,n}),
    downT (castTr Hm (rightT (castTc Hn M))) =
      rightT ( castTc Hn (downT (castTr Hm M))).
Proof. easy. Qed.

Lemma upT_flipT :
   {m n1 n2} (M : 'E^{m,n1 + n2}), upT (flipT M) = flipT (leftT M).
Proof. easy. Qed.

Lemma downT_flipT :
   {m n1 n2} (M : 'E^{m,n1 + n2}), downT (flipT M) = flipT (rightT M).
Proof. easy. Qed.

Lemma leftT_flipT :
   {m1 m2 n} (M : 'E^{m1 + m2,n}), leftT (flipT M) = flipT (upT M).
Proof. easy. Qed.

Lemma rightT_flipT :
   {m1 m2 n} (M : 'E^{m1 + m2,n}), rightT (flipT M) = flipT (downT M).
Proof. easy. Qed.

Lemma ulT_flipT :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}), ulT (flipT M) = flipT (ulT M).
Proof. easy. Qed.

Lemma urT_flipT :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}), urT (flipT M) = flipT (dlT M).
Proof. easy. Qed.

Lemma dlT_flipT :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}), dlT (flipT M) = flipT (urT M).
Proof. easy. Qed.

Lemma drT_flipT :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}), drT (flipT M) = flipT (drT M).
Proof. easy. Qed.

Lemma upT_concatTr :
   {m1 m2 n} (M1 : 'E^{m1,n}) (M2 : 'E^{m2,n}),
    upT (concatTr M1 M2) = M1.
Proof. intros; apply firstF_concatF. Qed.

Lemma downT_concatTr :
   {m1 m2 n} (M1 : 'E^{m1,n}) (M2 : 'E^{m2,n}),
    downT (concatTr M1 M2) = M2.
Proof. intros; apply lastF_concatF. Qed.

Lemma leftT_concatTc :
   {m n1 n2} (M1 : 'E^{m,n1}) (M2 : 'E^{m,n2}),
    leftT (concatTc M1 M2) = M1.
Proof. intros; apply extF; intro; apply firstF_concatF. Qed.

Lemma rightT_concatTc :
   {m n1 n2} (M1 : 'E^{m,n1}) (M2 : 'E^{m,n2}),
    rightT (concatTc M1 M2) = M2.
Proof. intros; apply extF; intro; apply lastF_concatF. Qed.

Lemma ulT_concatT :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}),
    ulT (concatT M11 M12 M21 M22) = M11.
Proof. intros; rewrite ulT_equiv_def upT_concatTr leftT_concatTc; easy. Qed.

Lemma urT_concatT :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}),
    urT (concatT M11 M12 M21 M22) = M12.
Proof. intros; rewrite urT_equiv_def upT_concatTr rightT_concatTc; easy. Qed.

Lemma dlT_concatT :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}),
    dlT (concatT M11 M12 M21 M22) = M21.
Proof. intros; rewrite dlT_equiv_def downT_concatTr leftT_concatTc; easy. Qed.

Lemma drT_concatT :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}),
    drT (concatT M11 M12 M21 M22) = M22.
Proof. intros; rewrite drT_equiv_def downT_concatTr rightT_concatTc; easy. Qed.

Lemma concatTr_splitTr :
   {m1 m2 n} (M : 'E^{m1 + m2,n}), M = concatTr (upT M) (downT M).
Proof. intros; apply concatF_splitF. Qed.

Lemma concatTc_splitTc :
   {m n1 n2} (M : 'E^{m,n1 + n2}), M = concatTc (leftT M) (rightT M).
Proof. intros; apply extF; intro; apply concatF_splitF. Qed.

Lemma concatT_splitT :
   {m1 m2 n1 n2} (M : 'E^{m1 + m2,n1 + n2}),
    M = concatT (ulT M) (urT M) (dlT M) (drT M).
Proof.
intros; unfold concatT; rewrite {1}(concatTr_splitTr M); f_equal.
rewrite ulT_equiv_def urT_equiv_def; apply concatTc_splitTc.
rewrite dlT_equiv_def drT_equiv_def; apply concatTc_splitTc.
Qed.

Lemma splitTr_compat :
   {m1 m2 n} (M N : 'E^{m1 + m2,n}),
    M = N upT M = upT N downT M = downT N.
Proof. intros; split; f_equal; easy. Qed.

Lemma splitTc_compat :
   {m n1 n2} (M N : 'E^{m,n1 + n2}),
    M = N leftT M = leftT N rightT M = rightT N.
Proof. intros; split; f_equal; easy. Qed.

Lemma splitT_compat :
   {m1 m2 n1 n2} (M N : 'E^{m1 + m2,n1 + n2}),
    M = N ulT M = ulT N urT M = urT N dlT M = dlT N drT M = drT N.
Proof. intros; repeat split; f_equal; easy. Qed.

Lemma splitTr_reg :
   {m1 m2 n} (M N : 'E^{m1 + m2,n}),
    upT M = upT N downT M = downT N M = N.
Proof.
intros m1 m2 n M N Hu Hd.
rewrite (concatTr_splitTr M) Hu Hd -concatTr_splitTr; easy.
Qed.

Lemma splitTc_reg :
   {m n1 n2} (M N : 'E^{m,n1 + n2}),
    leftT M = leftT N rightT M = rightT N M = N.
Proof.
intros m n1 n2 M N Hl Hr.
rewrite (concatTc_splitTc M) Hl Hr -concatTc_splitTc; easy.
Qed.

Lemma splitT_reg :
   {m1 m2 n1 n2} (M N : 'E^{m1 + m2,n1 + n2}),
    ulT M = ulT N urT M = urT N dlT M = dlT N drT M = drT N M = N.
Proof.
intros m1 m2 n1 n2 M N Hul Hur Hdl Hdr.
rewrite (concatT_splitT M) Hul Hur Hdl Hdr -concatT_splitT; easy.
Qed.

Lemma extTr_splitTr :
   {m m1 m2 n} (Hm : m = m1 + m2) (M N : 'E^{m,n}),
    upT (castTr Hm M) = upT (castTr Hm N)
    downT (castTr Hm M) = downT (castTr Hm N)
    M = N.
Proof. intros m m1 m2 n; apply extF_splitF. Qed.

Lemma extTc_splitTc :
   {m n n1 n2} (Hn : n = n1 + n2) (M N : 'E^{m,n}),
    leftT (castTc Hn M) = leftT (castTc Hn N)
    rightT (castTc Hn M) = rightT (castTc Hn N)
    M = N.
Proof.
intros m n n1 n2 Hn M N Hl Hr; apply (castTc_inj Hn), splitTc_reg; easy.
Qed.

Lemma extT_splitT :
   {m m1 m2 n n1 n2} (Hm : m = m1 + m2) (Hn : n = n1 + n2)
      (M N : 'E^{m,n}),
    ulT (castT Hm Hn M) = ulT (castT Hm Hn N)
    urT (castT Hm Hn M) = urT (castT Hm Hn N)
    dlT (castT Hm Hn M) = dlT (castT Hm Hn N)
    drT (castT Hm Hn M) = drT (castT Hm Hn N)
    M = N.
Proof.
intros m m1 m2 n n1 n2 Hm Hn M N Hul Hur Hdl Hdr.
apply (castT_inj Hm Hn), splitT_reg; easy.
Qed.

Lemma upT_insertTr :
   {m n} (M : 'E^{m,n}) A i0,
    upT (castTr (ord_splitS i0) (insertTr M A i0)) =
    upT (castTr (ord_split i0) M).
Proof. intros; apply firstF_insertF. Qed.

Lemma downT_insertTr :
   {m n} (M : 'E^{m,n}) A i0,
    downT (castTr (ordS_splitS i0) (insertTr M A i0)) =
    downT (castTr (ord_split i0) M).
Proof. intros; apply lastF_insertF. Qed.

Lemma leftT_insertTc :
   {m n} (M : 'E^{m,n}) B j0,
    leftT (castTc (ord_splitS j0) (insertTc M B j0)) =
    leftT (castTc (ord_split j0) M).
Proof. intros; apply extF; intro; apply firstF_insertF. Qed.

Lemma rightT_insertTc :
   {m n} (M : 'E^{m,n}) B j0,
    rightT (castTc (ordS_splitS j0) (insertTc M B j0)) =
    rightT (castTc (ord_split j0) M).
Proof. intros; apply extF; intro; apply lastF_insertF. Qed.

Lemma ulT_insertT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    ulT (castT (ord_splitS i0) (ord_splitS j0) (insertT M A B x i0 j0)) =
    ulT (castT (ord_split i0) (ord_split j0) M).
Proof.
intros; unfold ulT; rewrite insertT_equiv_def 2!leftT_castTr leftT_insertTc.
rewrite 2!upT_leftT upT_insertTr; easy.
Qed.

Lemma urT_insertT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    urT (castT (ord_splitS i0) (ordS_splitS j0) (insertT M A B x i0 j0)) =
    urT (castT (ord_split i0) (ord_split j0) M).
Proof.
intros; unfold urT; rewrite insertT_equiv_def 2!rightT_castTr rightT_insertTc.
rewrite 2!upT_rightT upT_insertTr; easy.
Qed.

Lemma dlT_insertT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    dlT (castT (ordS_splitS i0) (ord_splitS j0) (insertT M A B x i0 j0)) =
    dlT (castT (ord_split i0) (ord_split j0) M).
Proof.
intros; unfold dlT; rewrite insertT_equiv_def 2!leftT_castTr leftT_insertTc.
rewrite 2!downT_leftT downT_insertTr; easy.
Qed.

Lemma drT_insertT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    drT (castT (ordS_splitS i0) (ordS_splitS j0) (insertT M A B x i0 j0)) =
    drT (castT (ord_split i0) (ord_split j0) M).
Proof.
intros; unfold drT; rewrite insertT_equiv_def 2!rightT_castTr rightT_insertTc.
rewrite 2!downT_rightT downT_insertTr; easy.
Qed.

Lemma upT_skipTr :
   {m n} (M : 'E^{m.+1,n}) i0,
    upT (castTr (ord_split i0) (skipTr M i0)) =
    upT (castTr (ord_splitS i0) M).
Proof. intros; apply firstF_skipF. Qed.

Lemma downT_skipTr :
   {m n} (M : 'E^{m.+1,n}) i0,
    downT (castTr (ord_split i0) (skipTr M i0)) =
    downT (castTr (ordS_splitS i0) M).
Proof. intros; apply lastF_skipF. Qed.

Lemma leftT_skipTc :
   {m n} (M : 'E^{m,n.+1}) j0,
    leftT (castTc (ord_split j0) (skipTc M j0)) =
    leftT (castTc (ord_splitS j0) M).
Proof. intros; apply extF; intro; apply firstF_skipF. Qed.

Lemma rightT_skipTc :
   {m n} (M : 'E^{m,n.+1}) j0,
    rightT (castTc (ord_split j0) (skipTc M j0)) =
    rightT (castTc (ordS_splitS j0) M).
Proof. intros; apply extF; intro; apply lastF_skipF. Qed.

Lemma ulT_skipT :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0,
    ulT (castT (ord_split i0) (ord_split j0) (skipT M i0 j0)) =
    ulT (castT (ord_splitS i0) (ord_splitS j0) M).
Proof.
intros; unfold ulT; rewrite skipT_equiv_def 2!leftT_castTr leftT_skipTc.
rewrite 2!upT_leftT upT_skipTr; easy.
Qed.

Lemma urT_skipT :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0,
    urT (castT (ord_split i0) (ord_split j0) (skipT M i0 j0)) =
    urT (castT (ord_splitS i0) (ordS_splitS j0) M).
Proof.
intros; unfold urT; rewrite skipT_equiv_def 2!rightT_castTr rightT_skipTc.
rewrite 2!upT_rightT upT_skipTr; easy.
Qed.

Lemma dlT_skipT :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0,
    dlT (castT (ord_split i0) (ord_split j0) (skipT M i0 j0)) =
    dlT (castT (ordS_splitS i0) (ord_splitS j0) M).
Proof.
intros; unfold dlT; rewrite skipT_equiv_def 2!leftT_castTr leftT_skipTc.
rewrite 2!downT_leftT downT_skipTr; easy.
Qed.

Lemma drT_skipT :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0,
    drT (castT (ord_split i0) (ord_split j0) (skipT M i0 j0)) =
    drT (castT (ordS_splitS i0) (ordS_splitS j0) M).
Proof.
intros; unfold drT; rewrite skipT_equiv_def 2!rightT_castTr rightT_skipTc.
rewrite 2!downT_rightT downT_skipTr; easy.
Qed.

Lemma upT_replaceTr :
   {m n} (M : 'E^{m,n}) A i0,
    upT (castTr (ord_split_pred i0) (replaceTr M A i0)) =
    upT (castTr (ord_split_pred i0) M).
Proof. intros; apply firstF_replaceF. Qed.

Lemma downT_replaceTr :
   {m n} (M : 'E^{m,n}) A i0,
    downT (castTr (ordS_split i0) (replaceTr M A i0)) =
    downT (castTr (ordS_split i0) M).
Proof. intros; apply lastF_replaceF. Qed.

Lemma leftT_replaceTc :
   {m n} (M : 'E^{m,n}) B j0,
    leftT (castTc (ord_split_pred j0) (replaceTc M B j0)) =
    leftT (castTc (ord_split_pred j0) M).
Proof. intros; apply extF; intro; apply firstF_replaceF. Qed.

Lemma rightT_replaceTc :
   {m n} (M : 'E^{m,n}) B j0,
    rightT (castTc (ordS_split j0) (replaceTc M B j0)) =
    rightT (castTc (ordS_split j0) M).
Proof. intros; apply extF; intro; apply lastF_replaceF. Qed.

Lemma ulT_replaceT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    ulT (castT (ord_split_pred i0) (ord_split_pred j0) (replaceT M A B x i0 j0)) =
    ulT (castT (ord_split_pred i0) (ord_split_pred j0) M).
Proof.
intros; unfold ulT; rewrite replaceT_equiv_def 2!leftT_castTr leftT_replaceTc.
rewrite 2!upT_leftT upT_replaceTr; easy.
Qed.

Lemma urT_replaceT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    urT (castT (ord_split_pred i0) (ordS_split j0) (replaceT M A B x i0 j0)) =
    urT (castT (ord_split_pred i0) (ordS_split j0) M).
Proof.
intros; unfold urT; rewrite replaceT_equiv_def 2!rightT_castTr rightT_replaceTc.
rewrite 2!upT_rightT upT_replaceTr; easy.
Qed.

Lemma dlT_replaceT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    dlT (castT (ordS_split i0) (ord_split_pred j0) (replaceT M A B x i0 j0)) =
    dlT (castT (ordS_split i0) (ord_split_pred j0) M).
Proof.
intros; unfold dlT; rewrite replaceT_equiv_def 2!leftT_castTr leftT_replaceTc.
rewrite 2!downT_leftT downT_replaceTr; easy.
Qed.

Lemma drT_replaceT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    drT (castT (ordS_split i0) (ordS_split j0) (replaceT M A B x i0 j0)) =
    drT (castT (ordS_split i0) (ordS_split j0) M).
Proof.
intros; unfold drT; rewrite replaceT_equiv_def 2!rightT_castTr rightT_replaceTc.
rewrite 2!downT_rightT downT_replaceTr; easy.
Qed.

Properties of operators concatTr/concatTc/concatT.

Lemma concatTr_flipT :
   {m n1 n2} (M1 : 'E^{m,n1}) (M2 : 'E^{m,n2}),
    concatTr (flipT M1) (flipT M2) = flipT (concatTc M1 M2).
Proof.
intros m n1 n2 M1 M2; apply extT; intros i j; unfold flipT.
destruct (lt_dec i n1) as [Hi | Hi].
rewrite concatTr_correct_u concatTc_correct_l; easy.
rewrite concatTr_correct_d concatTc_correct_r; easy.
Qed.

Lemma concatTc_flipT :
   {m1 m2 n} (M1 : 'E^{m1,n}) (M2 : 'E^{m2,n}),
    concatTc (flipT M1) (flipT M2) = flipT (concatTr M1 M2).
Proof. intros; apply flipT_inj; rewrite flipT_invol concatTr_flipT; easy. Qed.

Lemma concatT_flipT :
   {m1 m2 n1 n2} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}),
    concatT (flipT M11) (flipT M21) (flipT M12) (flipT M22) =
      flipT (concatT M11 M12 M21 M22).
Proof.
intros; rewrite concatT_equiv_def; unfold concatT.
rewrite 2!concatTr_flipT concatTc_flipT; easy.
Qed.

Lemma concatTr_eq :
   {m1 m2 n} (M1 N1 : 'E^{m1,n}) (M2 N2 : 'E^{m2,n}),
    M1 = N1 M2 = N2 concatTr M1 M2 = concatTr N1 N2.
Proof. intros; f_equal; easy. Qed.

Lemma concatTc_eq :
   {m n1 n2} (M1 N1 : 'E^{m,n1}) (M2 N2 : 'E^{m,n2}),
    M1 = N1 M2 = N2 concatTc M1 M2 = concatTc N1 N2.
Proof. intros; f_equal; easy. Qed.

Lemma concatT_eq :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) (M12 N12 : 'E^{m1,n2})
      (M21 N21 : 'E^{m2,n1}) (M22 N22 : 'E^{m2,n2}),
    M11 = N11 M12 = N12 M21 = N21 M22 = N22
    concatT M11 M12 M21 M22 = concatT N11 N12 N21 N22.
Proof. intros; f_equal; easy. Qed.

Lemma concatTr_inj_u :
   {m1 m2 n} (M1 N1 : 'E^{m1,n}) (M2 N2 : 'E^{m2,n}),
    concatTr M1 M2 = concatTr N1 N2 M1 = N1.
Proof. intros m1 m2 n M1 N1 M2 N2; apply concatF_inj_l. Qed.

Lemma concatTr_inj_d :
   {m1 m2 n} (M1 N1 : 'E^{m1,n}) (M2 N2 : 'E^{m2,n}),
    concatTr M1 M2 = concatTr N1 N2 M2 = N2.
Proof. intros m1 m2 n M1 N1 M2 N2; apply concatF_inj_r. Qed.

Lemma concatTr_inj :
   {m1 m2 n} (M1 N1 : 'E^{m1,n}) (M2 N2 : 'E^{m2,n}),
    concatTr M1 M2 = concatTr N1 N2 M1 = N1 M2 = N2.
Proof. intros m1 m2 n M1 N1 M2 N2; apply concatF_inj. Qed.

Lemma concatTc_inj_l :
   {m n1 n2} (M1 N1 : 'E^{m,n1}) (M2 N2 : 'E^{m,n2}),
    concatTc M1 M2 = concatTc N1 N2 M1 = N1.
Proof.
intros m n1 n2 M1 N1 M2 N2 H.
apply flipT_inj, (concatTr_inj_u _ _ (flipT M2) (flipT N2)), flipT_inj.
rewrite -2!concatTc_flipT 4!flipT_invol; easy.
Qed.

Lemma concatTc_inj_r :
   {m n1 n2} (M1 N1 : 'E^{m,n1}) (M2 N2 : 'E^{m,n2}),
    concatTc M1 M2 = concatTc N1 N2 M2 = N2.
Proof.
intros m n1 n2 M1 N1 M2 N2 H.
apply flipT_inj, (concatTr_inj_d (flipT M1) (flipT N1)), flipT_inj.
rewrite -2!concatTc_flipT 4!flipT_invol; easy.
Qed.

Lemma concatTc_inj :
   {m n1 n2} (M1 N1 : 'E^{m,n1}) (M2 N2 : 'E^{m,n2}),
    concatTc M1 M2 = concatTc N1 N2 M1 = N1 M2 = N2.
Proof.
intros m n1 n2 M1 N1 M2 N2 H; split; generalize H; clear H;
    [apply concatTc_inj_l | apply concatTc_inj_r].
Qed.

Lemma concatT_inj_ul :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) (M12 N12 : 'E^{m1,n2})
      (M21 N21 : 'E^{m2,n1}) (M22 N22 : 'E^{m2,n2}),
    concatT M11 M12 M21 M22 = concatT N11 N12 N21 N22 M11 = N11.
Proof. move=>> H; eapply concatTc_inj_l, concatTr_inj_u; apply H. Qed.

Lemma concatT_inj_ur :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) (M12 N12 : 'E^{m1,n2})
      (M21 N21 : 'E^{m2,n1}) (M22 N22 : 'E^{m2,n2}),
    concatT M11 M12 M21 M22 = concatT N11 N12 N21 N22 M12 = N12.
Proof. move=>> H; eapply concatTc_inj_r, concatTr_inj_u; apply H. Qed.

Lemma concatT_inj_dl :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) (M12 N12 : 'E^{m1,n2})
      (M21 N21 : 'E^{m2,n1}) (M22 N22 : 'E^{m2,n2}),
    concatT M11 M12 M21 M22 = concatT N11 N12 N21 N22 M21 = N21.
Proof. move=>> H; eapply concatTc_inj_l, concatTr_inj_d; apply H. Qed.

Lemma concatT_inj_dr :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) (M12 N12 : 'E^{m1,n2})
      (M21 N21 : 'E^{m2,n1}) (M22 N22 : 'E^{m2,n2}),
    concatT M11 M12 M21 M22 = concatT N11 N12 N21 N22 M22 = N22.
Proof. move=>> H; eapply concatTc_inj_r, concatTr_inj_d; apply H. Qed.

Lemma concatT_inj :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) (M12 N12 : 'E^{m1,n2})
      (M21 N21 : 'E^{m2,n1}) (M22 N22 : 'E^{m2,n2}),
    concatT M11 M12 M21 M22 = concatT N11 N12 N21 N22
    M11 = N11 M12 = N12 M21 = N21 M22 = N22.
Proof.
move=>> H; repeat split.
eapply concatT_inj_ul; apply H.
eapply concatT_inj_ur; apply H.
eapply concatT_inj_dl; apply H.
eapply concatT_inj_dr; apply H.
Qed.

Lemma concatTr_nextT_compat_u :
   {m1 m2 n} {M1 N1 : 'E^{m1,n}} (M2 N2 : 'E^{m2,n}),
    M1 N1 concatTr M1 M2 concatTr N1 N2.
Proof. intros; apply concatF_nextF_compat_l; easy. Qed.

Lemma concatTr_nextT_compat_d :
   {m1 m2 n} (M1 N1 : 'E^{m1,n}) {M2 N2 : 'E^{m2,n}},
    M2 N2 concatTr M1 M2 concatTr N1 N2.
Proof. intros; apply concatF_nextF_compat_r; easy. Qed.

Lemma concatTr_nextT_reg :
   {m1 m2 n} {M1 N1 : 'E^{m1,n}} {M2 N2 : 'E^{m2,n}},
    concatTr M1 M2 concatTr N1 N2 M1 N1 M2 N2.
Proof. intros; apply concatF_nextF_reg; easy. Qed.

Lemma concatTr_nextT_equiv :
   {m1 m2 n} {M1 N1 : 'E^{m1,n}} {M2 N2 : 'E^{m2,n}},
    concatTr M1 M2 concatTr N1 N2 M1 N1 M2 N2.
Proof.
intros; split; [apply concatTr_nextT_reg | intros [H | H]];
    [apply concatTr_nextT_compat_u | apply concatTr_nextT_compat_d]; easy.
Qed.

Lemma concatTc_nextT_compat_l :
   {m n1 n2} {M1 N1 : 'E^{m,n1}} (M2 N2 : 'E^{m,n2}),
    M1 N1 concatTc M1 M2 concatTc N1 N2.
Proof. move=>> H; contradict H; eapply concatTc_inj_l; apply H. Qed.

Lemma concatTc_nextT_compat_r :
   {m n1 n2} (M1 N1 : 'E^{m,n1}) {M2 N2 : 'E^{m,n2}},
    M2 N2 concatTc M1 M2 concatTc N1 N2.
Proof. move=>> H; contradict H; eapply concatTc_inj_r; apply H. Qed.

Lemma concatTc_nextT_reg :
   {m n1 n2} {M1 N1 : 'E^{m,n1}} {M2 N2 : 'E^{m,n2}},
    concatTc M1 M2 concatTc N1 N2 M1 N1 M2 N2.
Proof.
move=>> H; apply not_and_or; contradict H; apply concatTc_eq; easy.
Qed.

Lemma concatTc_nextT_equiv :
   {m n1 n2} {M1 N1 : 'E^{m,n1}} {M2 N2 : 'E^{m,n2}},
    concatTc M1 M2 concatTc N1 N2 M1 N1 M2 N2.
Proof.
intros; split; [apply concatTc_nextT_reg | intros [H | H]];
    [apply concatTc_nextT_compat_l | apply concatTc_nextT_compat_r]; easy.
Qed.

Lemma concatT_nextT_compat_ul :
   {m1 m2 n1 n2} {M11 N11 : 'E^{m1,n1}} (M12 N12 : 'E^{m1,n2})
      (M21 N21 : 'E^{m2,n1}) (M22 N22 : 'E^{m2,n2}),
    M11 N11 concatT M11 M12 M21 M22 concatT N11 N12 N21 N22.
Proof. move=>> H; contradict H; eapply concatT_inj_ul; apply H. Qed.

Lemma concatT_nextT_compat_ur :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) {M12 N12 : 'E^{m1,n2}}
      (M21 N21 : 'E^{m2,n1}) (M22 N22 : 'E^{m2,n2}),
    M12 N12 concatT M11 M12 M21 M22 concatT N11 N12 N21 N22.
Proof. move=>> H; contradict H; eapply concatT_inj_ur; apply H. Qed.

Lemma concatT_nextT_compat_dl :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) (M12 N12 : 'E^{m1,n2})
      {M21 N21 : 'E^{m2,n1}} (M22 N22 : 'E^{m2,n2}),
    M21 N21 concatT M11 M12 M21 M22 concatT N11 N12 N21 N22.
Proof. move=>> H; contradict H; eapply concatT_inj_dl; apply H. Qed.

Lemma concatT_nextT_compat_dr :
   {m1 m2 n1 n2} (M11 N11 : 'E^{m1,n1}) (M12 N12 : 'E^{m1,n2})
      (M21 N21 : 'E^{m2,n1}) {M22 N22 : 'E^{m2,n2}},
    M22 N22 concatT M11 M12 M21 M22 concatT N11 N12 N21 N22.
Proof. move=>> H; contradict H; eapply concatT_inj_dr; apply H. Qed.

Lemma concatT_nextT_reg :
   {m1 m2 n1 n2} {M11 N11 : 'E^{m1,n1}} {M12 N12 : 'E^{m1,n2}}
      {M21 N21 : 'E^{m2,n1}} {M22 N22 : 'E^{m2,n2}},
    concatT M11 M12 M21 M22 concatT N11 N12 N21 N22
    M11 N11 M12 N12 M21 N21 M22 N22.
Proof.
move=>> H; apply not_and4_equiv; contradict H; apply concatT_eq; easy.
Qed.

Lemma concatT_nextT_equiv :
   {m1 m2 n1 n2} {M11 N11 : 'E^{m1,n1}} {M12 N12 : 'E^{m1,n2}}
      {M21 N21 : 'E^{m2,n1}} {M22 N22 : 'E^{m2,n2}},
    concatT M11 M12 M21 M22 concatT N11 N12 N21 N22
    M11 N11 M12 N12 M21 N21 M22 N22.
Proof.
intros; split; [apply concatT_nextT_reg | intros [H | [H | [H | H]]]];
    [apply concatT_nextT_compat_ul | apply concatT_nextT_compat_ur |
     apply concatT_nextT_compat_dl | apply concatT_nextT_compat_dr]; easy.
Qed.

Lemma concatTr_nil_u :
   {m2 n} (M1 : 'E^{0,n}) (M2 : 'E^{m2,n}), concatTr M1 M2 = M2.
Proof. intros; apply concatF_nil_l. Qed.

Lemma concatTr_nil_d :
   {m1 n} (M1 : 'E^{m1,n}) (M2 : 'E^{0,n}),
    concatTr M1 M2 = castTr (addn0_sym m1) M1.
Proof. intros; apply concatF_nil_r. Qed.

Lemma concatTc_nil_l :
   {m n2} (M1 : 'E^{m,0}) (M2 : 'E^{m,n2}), concatTc M1 M2 = M2.
Proof. intros; apply extF; intro; apply concatF_nil_l. Qed.

Lemma concatTc_nil_r :
   {m n1} (M1 : 'E^{m,n1}) (M2 : 'E^{m,0}),
    concatTc M1 M2 = castTc (addn0_sym n1) M1.
Proof. intros; apply extF; intro; apply concatF_nil_r. Qed.

Lemma concatT_nil_ul :
   {m2 n2} (M11 : 'E^{0,0}) (M12 : 'E^{0,n2})
      (M21 : 'E^{m2,0}) (M22 : 'E^{m2,n2}),
    concatT M11 M12 M21 M22 = M22.
Proof.
intros; unfold concatT; rewrite 2!concatTc_nil_l; apply concatTr_nil_u.
Qed.

Lemma concatT_nil_ur :
   {m2 n1} (M11 : 'E^{0,n1}) (M12 : 'E^{0,0})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,0}),
    concatT M11 M12 M21 M22 = castTc (addn0_sym n1) M21.
Proof.
intros; unfold concatT; rewrite 2!concatTc_nil_r; apply concatTr_nil_u.
Qed.

Lemma concatT_nil_dl :
   {m1 n2} (M11 : 'E^{m1,0}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{0,0}) (M22 : 'E^{0,n2}),
    concatT M11 M12 M21 M22 = castTr (addn0_sym m1) M12.
Proof.
intros; unfold concatT; rewrite 2!concatTc_nil_l; apply concatTr_nil_d.
Qed.

Lemma concatT_nil_dr :
   {m1 n1} (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,0})
      (M21 : 'E^{0,n1}) (M22 : 'E^{0,0}),
    concatT M11 M12 M21 M22 = castT (addn0_sym m1) (addn0_sym n1) M11.
Proof.
intros; unfold concatT; rewrite 2!concatTc_nil_r; apply concatTr_nil_d.
Qed.

Lemma concatT_blk1T_4 :
   (x00 x01 x10 x11 : E),
    concatT (blk1T x00) (blk1T x01) (blk1T x10) (blk1T x11) =
      blk2T x00 x01 x10 x11.
Proof.
intros; unfold blk2T, concatT, concatTr; rewrite -3!concatF_singleF_2; f_equal.
Qed.

Lemma concatTr_castTr :
   {m1 m2 m1' m2' n} (Hm1 : m1 = m1') (Hm2 : m2 = m2')
      (M1 : 'E^{m1,n}) (M2 : 'E^{m2,n}),
    concatTr (castTr Hm1 M1) (castTr Hm2 M2) =
      castTr (f_equal2_plus _ _ _ _ Hm1 Hm2) (concatTr M1 M2).
Proof. intros; apply concatF_castF. Qed.

Lemma concatTc_castTc :
   {m n1 n2 n1' n2'} (Hn1 : n1 = n1') (Hn2 : n2 = n2')
      (M1 : 'E^{m,n1}) (M2 : 'E^{m,n2}),
    concatTc (castTc Hn1 M1) (castTc Hn2 M2) =
      castTc (f_equal2_plus _ _ _ _ Hn1 Hn2) (concatTc M1 M2).
Proof. intros; apply extF; intro; apply concatF_castF. Qed.

Lemma concatT_castT :
   {m1 m2 m1' m2' n1 n2 n1' n2'}
      (Hm1 : m1 = m1') (Hm2 : m2 = m2') (Hn1 : n1 = n1') (Hn2 : n2 = n2')
      (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2})
      (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}),
    concatT (castT Hm1 Hn1 M11) (castT Hm1 Hn2 M12)
        (castT Hm2 Hn1 M21) (castT Hm2 Hn2 M22) =
      castT (f_equal2_plus _ _ _ _ Hm1 Hm2) (f_equal2_plus _ _ _ _ Hn1 Hn2)
        (concatT M11 M12 M21 M22).
Proof.
intros; subst; apply extT; move=>>; rewrite 4!castT_refl.
unfold castT, castTr, castTc, castF, mapF, mapiF; f_equal; apply ord_inj; easy.
Qed.

Lemma concatTr_castTc :
   {m1 m2 n1 n2} (Hn : n1 = n2) (M1 : 'E^{m1,n1}) (M2 : 'E^{m2,n1}),
    concatTr (castTc Hn M1) (castTc Hn M2) = castTc Hn (concatTr M1 M2).
Proof.
intros m1 m2 n1 n2; intros; subst n1; rewrite 3!castTc_refl; easy.
Qed.

Lemma concatTc_castTr :
   {m1 m2 n1 n2} (Hm : m1 = m2) (M1 : 'E^{m1,n1}) (M2 : 'E^{m1,n2}),
    concatTc (castTr Hm M1) (castTr Hm M2) = castTr Hm (concatTc M1 M2).
Proof.
intros m1 m2 n1 n2; intros; subst m1; rewrite 3!castTr_refl; easy.
Qed.

Lemma upT_concatTc :
   {m1 m2 n1 n2} (M1 : 'E^{m1 + m2,n1}) (M2 : 'E^{m1 + m2,n2}),
    upT (concatTc M1 M2) = concatTc (upT M1) (upT M2).
Proof. easy. Qed.

Lemma downT_concatTc :
   {m1 m2 n1 n2} (M1 : 'E^{m1 + m2,n1}) (M2 : 'E^{m1 + m2,n2}),
    downT (concatTc M1 M2) = concatTc (downT M1) (downT M2).
Proof. easy. Qed.

Lemma leftT_concatTr :
   {m1 m2 n1 n2} (M1 : 'E^{m1,n1 + n2}) (M2 : 'E^{m2,n1 + n2}),
    leftT (concatTr M1 M2) = concatTr (leftT M1) (leftT M2).
Proof.
intros; apply flipT_inj; rewrite -upT_flipT -2!concatTc_flipT; easy.
Qed.

Lemma rightT_concatTr :
   {m1 m2 n1 n2} (M1 : 'E^{m1,n1 + n2}) (M2 : 'E^{m2,n1 + n2}),
    rightT (concatTr M1 M2) = concatTr (rightT M1) (rightT M2).
Proof.
intros; apply flipT_inj; rewrite -downT_flipT -2!concatTc_flipT; easy.
Qed.

Properties of operators widenTr_S/widenTc_S/widenT_S/ liftTr_S/liftTc_S/liftT_S.

Lemma widenTr_S_flipT :
   {m n} (M : 'E^{m,n.+1}), widenTr_S (flipT M) = flipT (widenTc_S M).
Proof. easy. Qed.

Lemma liftTr_S_flipT :
   {m n} (M : 'E^{m,n.+1}), liftTr_S (flipT M) = flipT (liftTc_S M).
Proof. easy. Qed.

Lemma widenTc_S_flipT :
   {m n} (M : 'E^{m.+1,n}), widenTc_S (flipT M) = flipT (widenTr_S M).
Proof. easy. Qed.

Lemma liftTc_S_flipT :
   {m n} (M : 'E^{m.+1,n}), liftTc_S (flipT M) = flipT (liftTr_S M).
Proof. easy. Qed.

Lemma widenT_S_flipT :
   {m n} (M : 'E^{m.+1,n.+1}), widenT_S (flipT M) = flipT (widenT_S M).
Proof. easy. Qed.

Lemma liftT_S_flipT :
   {m n} (M : 'E^{m.+1,n.+1}), liftT_S (flipT M) = flipT (liftT_S M).
Proof. easy. Qed.

Properties of operators insertTr/insertTc/insertT.

Lemma insertTr_eq_gen :
   {m n} (M N : 'E^{m,n}) A C i0 k0,
    M = N A = C i0 = k0 insertTr M A i0 = insertTr N C k0.
Proof. intros; f_equal; easy. Qed.

Lemma insertTc_eq_gen :
   {m n} (M N : 'E^{m,n}) B D j0 l0,
    M = N B = D j0 = l0 insertTc M B j0 = insertTc N D l0.
Proof. intros; f_equal; easy. Qed.

Lemma insertT_eq_gen :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0 k0 l0,
    M = N A = C B = D x = y i0 = k0 j0 = l0
    insertT M A B x i0 j0 = insertT N C D y k0 l0.
Proof. intros; f_equal; easy. Qed.

Lemma insertTr_eq :
   {m n} (M N : 'E^{m,n}) A C i0,
    M = N A = C insertTr M A i0 = insertTr N C i0.
Proof. intros; f_equal; easy. Qed.

Lemma insertTc_eq :
   {m n} (M N : 'E^{m,n}) B D j0,
    M = N B = D insertTc M B j0 = insertTc N D j0.
Proof. intros; f_equal; easy. Qed.

Lemma insertT_eq :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    M = N A = C B = D x = y
    insertT M A B x i0 j0 = insertT N C D y i0 j0.
Proof. intros; f_equal; easy. Qed.

Lemma insertTr_inj_l :
   {m n} (M N : 'E^{m,n}) A C i0,
    insertTr M A i0 = insertTr N C i0 M = N.
Proof. move=>> H; eapply insertF_inj_l; apply H. Qed.

Lemma insertTr_inj_r :
   {m n} (M N : 'E^{m,n}) A C i0,
    insertTr M A i0 = insertTr N C i0 A = C.
Proof. move=>> H; eapply insertF_inj_r; apply H. Qed.

Lemma insertTr_inj :
   {m n} (M N : 'E^{m,n}) A C i0,
    insertTr M A i0 = insertTr N C i0 M = N A = C.
Proof. move=>> H; eapply insertF_inj; apply H. Qed.

Lemma insertTc_inj_l :
   {m n} (M N : 'E^{m,n}) B D j0,
    insertTc M B j0 = insertTc N D j0 M = N.
Proof.
move=>> /extF_rev H; apply extF; intro; eapply insertF_inj_l; apply H.
Qed.

Lemma insertTc_inj_r :
   {m n} (M N : 'E^{m,n}) B D j0,
    insertTc M B j0 = insertTc N D j0 B = D.
Proof.
move=>> /extF_rev H; apply extF; intro; eapply insertF_inj_r; apply H.
Qed.

Lemma insertTc_inj :
   {m n} (M N : 'E^{m,n}) B D j0,
    insertTc M B j0 = insertTc N D j0 M = N B = D.
Proof.
move=>> H; split; [eapply insertTc_inj_l | eapply insertTc_inj_r]; apply H.
Qed.

Lemma insertT_inj_l :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    insertT M A B x i0 j0 = insertT N C D y i0 j0 M = N.
Proof. move=>> H; eapply insertTc_inj_l, insertTr_inj_l; apply H. Qed.

Lemma insertT_inj_ml :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    insertT M A B x i0 j0 = insertT N C D y i0 j0 A = C.
Proof. move=>> /insertTr_inj_r H; eapply insertF_inj_l; apply H. Qed.

Lemma insertT_inj_mr :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    insertT M A B x i0 j0 = insertT N C D y i0 j0 B = D.
Proof. move=>> /insertTr_inj_l H; eapply insertTc_inj_r; apply H. Qed.

Lemma insertT_inj_r :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    insertT M A B x i0 j0 = insertT N C D y i0 j0 x = y.
Proof. move=>> /insertTr_inj_r H; eapply insertF_inj_r; apply H. Qed.

Lemma insertT_inj :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    insertT M A B x i0 j0 = insertT N C D y i0 j0
    M = N A = C B = D x = y.
Proof.
move=>> H; repeat split;
    [eapply insertT_inj_l | eapply insertT_inj_ml |
     eapply insertT_inj_mr | eapply insertT_inj_r]; apply H.
Qed.

Lemma insertTr_nextT_compat_l :
   {m n} {M N : 'E^{m,n}} A C i0,
    M N insertTr M A i0 insertTr N C i0.
Proof. move=>>; apply insertF_nextF_compat_l. Qed.

Lemma insertTr_nextT_compat_r :
   {m n} (M N : 'E^{m,n}) {A C} i0,
    A C insertTr M A i0 insertTr N C i0.
Proof. move=>>; apply insertF_nextF_compat_r. Qed.

Lemma insertTr_nextT_reg :
   {m n} {M N : 'E^{m,n}} {A C} i0,
    insertTr M A i0 insertTr N C i0 M N A C.
Proof. move=>>; apply insertF_nextF_reg. Qed.

Lemma insertTr_nextT_equiv :
   {m n} {M N : 'E^{m,n}} {A C} i0,
    insertTr M A i0 insertTr N C i0 M N A C.
Proof.
intros; split; [apply insertTr_nextT_reg | intros [H | H]];
    [apply insertTr_nextT_compat_l | apply insertTr_nextT_compat_r]; easy.
Qed.

Lemma insertTc_nextT_compat_l :
   {m n} {M N : 'E^{m,n}} B D j0,
    M N insertTc M B j0 insertTc N D j0.
Proof. move=>> H; contradict H; apply insertTc_inj in H; easy. Qed.

Lemma insertTc_nextT_compat_r :
   {m n} (M N : 'E^{m,n}) {B D} j0,
    B D insertTc M B j0 insertTc N D j0.
Proof. move=>> H; contradict H; apply insertTc_inj in H; easy. Qed.

Lemma insertTc_nextT_reg :
   {m n} {M N : 'E^{m,n}} {B D} j0,
    insertTc M B j0 insertTc N D j0 M N B D.
Proof.
move=>>; rewrite -not_and_equiv -contra_equiv.
intros; apply insertTc_eq; easy.
Qed.

Lemma insertTc_nextT_equiv :
   {m n} {M N : 'E^{m,n}} {B D} j0,
    insertTc M B j0 insertTc N D j0 M N B D.
Proof.
intros; split; [apply insertTc_nextT_reg | intros [H | H]];
    [apply insertTc_nextT_compat_l | apply insertTc_nextT_compat_r]; easy.
Qed.

Lemma insertT_nextT_compat_l :
   {m n} {M N : 'E^{m,n}} A B C D x y i0 j0,
    M N insertT M A B x i0 j0 insertT N C D y i0 j0.
Proof. move=>> H; contradict H; apply insertT_inj in H; easy. Qed.

Lemma insertT_nextT_compat_ml :
   {m n} (M N : 'E^{m,n}) {A} B {C} D x y i0 j0,
    A C insertT M A B x i0 j0 insertT N C D y i0 j0.
Proof. move=>> H; contradict H; apply insertT_inj in H; easy. Qed.

Lemma insertT_nextT_compat_mr :
   {m n} (M N : 'E^{m,n}) A {B} C {D} x y i0 j0,
    B D insertT M A B x i0 j0 insertT N C D y i0 j0.
Proof. move=>> H; contradict H; apply insertT_inj in H; easy. Qed.

Lemma insertT_nextT_compat_r :
   {m n} (M N : 'E^{m,n}) A B C D {x y} i0 j0,
    x y insertT M A B x i0 j0 insertT N C D y i0 j0.
Proof. move=>> H; contradict H; apply insertT_inj in H; easy. Qed.

Lemma insertT_nextT_reg :
   {m n} {M N : 'E^{m,n}} {A B C D x y} i0 j0,
    insertT M A B x i0 j0 insertT N C D y i0 j0
    M N A C B D x y.
Proof.
move=>>; rewrite -not_and4_equiv -contra_equiv.
intros; apply insertT_eq; easy.
Qed.

Lemma insertT_nextT_equiv :
   {m n} {M N : 'E^{m,n}} {A B C D x y} i0 j0,
    insertT M A B x i0 j0 insertT N C D y i0 j0
    M N A C B D x y.
Proof.
intros; split; [apply insertT_nextT_reg | intros [H | [H | [H | H]]]];
    [apply insertT_nextT_compat_l | apply insertT_nextT_compat_ml |
     apply insertT_nextT_compat_mr | apply insertT_nextT_compat_r]; easy.
Qed.

Lemma insertTr_constT :
   {m n} (x : E) i0,
    insertTr (constT m n x) (constF n x) i0 = constT m.+1 n x.
Proof. intros; apply insertF_constF. Qed.

Lemma insertTc_constT :
   {m n} (x : E) j0,
    insertTc (constT m n x) (constF m x) j0 = constT m n.+1 x.
Proof. intros; apply extF; intro; apply insertF_constF. Qed.

Lemma insertT_constT :
   {m n} (x : E) i0 j0,
    insertT (constT m n x) (constF n x) (constF m x) x i0 j0 =
      constT m.+1 n.+1 x.
Proof.
intros; unfold insertT; rewrite insertTc_constT insertF_constF.
apply insertTr_constT.
Qed.

Lemma flipT_insertTr :
   {m n} (M : 'E^{m,n}) A i0,
    flipT (insertTr M A i0) = insertTc (flipT M) A i0.
Proof.
intros m n M B j0; apply extT; intros i j.
unfold insertTr, insertTc, flipT; destruct (ord_eq_dec j j0).
rewrite → 2!insertF_correct_l; easy.
rewrite 2!insertF_correct_r; easy.
Qed.

Lemma flipT_insertTc :
   {m n} (M : 'E^{m,n}) B j0,
    flipT (insertTc M B j0) = insertTr (flipT M) B j0.
Proof. intros; apply flipT_inj; rewrite flipT_insertTr; easy. Qed.

Lemma flipT_insertT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    flipT (insertT M A B x i0 j0) = insertT (flipT M) B A x j0 i0.
Proof. intros; rewrite insertT_equiv_def flipT_insertTc flipT_insertTr; easy. Qed.

Properties of operators skipTr/skipTc/skipT.

Lemma flipT_skipTr :
   {m n} (M : 'E^{m.+1,n}) i0, flipT (skipTr M i0) = skipTc (flipT M) i0.
Proof. easy. Qed.

Lemma flipT_skipTc :
   {m n} (M : 'E^{m,n.+1}) j0, flipT (skipTc M j0) = skipTr (flipT M) j0.
Proof. easy. Qed.

Lemma flipT_skipT :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0,
    flipT (skipT M i0 j0) = skipT (flipT M) j0 i0.
Proof. easy. Qed.

Lemma skipTr_compat_gen :
   {m n} (M N : 'E^{m.+1,n}) i0 k0,
    eqxTr M N i0 i0 = k0 skipTr M i0 = skipTr N k0.
Proof. intros; apply skipF_compat_gen; easy. Qed.

Lemma skipTc_compat_gen :
   {m n} (M N : 'E^{m,n.+1}) j0 l0,
    eqxTc M N j0 j0 = l0 skipTc M j0 = skipTc N l0.
Proof. intros; apply extF; intro; apply skipF_compat_gen; easy. Qed.

Lemma skipT_compat_gen :
   {m n} (M N : 'E^{m.+1,n.+1}) i0 j0 k0 l0,
    eqxT M N i0 j0 i0 = k0 j0 = l0 skipT M i0 j0 = skipT N k0 l0.
Proof.
intros; apply skipTr_compat_gen; try easy; intros i Hi.
apply skipF_compat_gen; try easy; intros j Hj; auto.
Qed.

Lemma skipTr_compat :
   {m n} (M N : 'E^{m.+1,n}) i0,
    eqxTr M N i0 skipTr M i0 = skipTr N i0.
Proof. intros; apply skipTr_compat_gen; easy. Qed.

Lemma skipTc_compat :
   {m n} (M N : 'E^{m,n.+1}) j0,
    eqxTc M N j0 skipTc M j0 = skipTc N j0.
Proof. intros; apply skipTc_compat_gen; easy. Qed.

Lemma skipT_compat :
   {m n} (M N : 'E^{m.+1,n.+1}) i0 j0,
    eqxT M N i0 j0 skipT M i0 j0 = skipT N i0 j0.
Proof. intros; apply skipT_compat_gen; easy. Qed.

Lemma skipTr_reg :
   {m n} (M N : 'E^{m.+1,n}) i0,
    skipTr M i0 = skipTr N i0 eqxTr M N i0.
Proof. intros m n M N i0; apply (skipF_reg _ _ i0); easy. Qed.

Lemma skipTc_reg :
   {m n} (M N : 'E^{m,n.+1}) j0,
    skipTc M j0 = skipTc N j0 eqxTc M N j0.
Proof.
intros; apply eqxTr_flipT, skipTr_reg.
rewrite -2!flipT_skipTc; apply flipT_eq; easy.
Qed.

Lemma skipT_reg :
   {m n} (M N : 'E^{m.+1,n.+1}) i0 j0,
    skipT M i0 j0 = skipT N i0 j0 eqxT M N i0 j0.
Proof.
intros m n M N i0 j0 H i j Hi Hj.
apply (skipF_reg _ _ j0); try easy.
apply (skipF_reg (skipTc M _) (skipTc N _) i0); easy.
Qed.

Lemma eqxTr_equiv :
   {m n} (M N : 'E^{m.+1,n}) i0,
    eqxTr M N i0 skipTr M i0 = skipTr N i0.
Proof. intros; apply eqxF_equiv. Qed.

Lemma eqxTc_equiv :
   {m n} (M N : 'E^{m,n.+1}) j0,
    eqxTc M N j0 skipTc M j0 = skipTc N j0.
Proof. intros; split. intros; apply skipTc_compat; easy. apply skipTc_reg. Qed.

Lemma eqxT_equiv :
   {m n} (M N : 'E^{m.+1,n.+1}) i0 j0,
    eqxT M N i0 j0 skipT M i0 j0 = skipT N i0 j0.
Proof. intros; split. intros; apply skipT_compat; easy. apply skipT_reg. Qed.

Lemma skipTr_neqxTr_compat :
   {m n} {M N : 'E^{m.+1,n}} {i0},
    neqxTr M N i0 skipTr M i0 skipTr N i0.
Proof. move=>>; apply skipF_neqxF_compat. Qed.

Lemma skipTr_neqxTr_reg :
   {m n} {M N : 'E^{m.+1,n}} {i0},
    skipTr M i0 skipTr N i0 neqxTr M N i0.
Proof. move=>>; apply skipF_neqxF_reg. Qed.

Lemma skipTc_neqxTc_compat :
   {m n} {M N : 'E^{m,n.+1}} {j0},
    neqxTc M N j0 skipTc M j0 skipTc N j0.
Proof.
move=>>; rewrite contra_not_r_equiv -eqxTc_not_equiv; apply skipTc_reg.
Qed.

Lemma skipTc_neqxTc_reg :
   {m n} {M N : 'E^{m,n.+1}} {j0},
    skipTc M j0 skipTc N j0 neqxTc M N j0.
Proof.
move=>>; rewrite contra_not_l_equiv -eqxTc_not_equiv; apply skipTc_compat.
Qed.

Lemma skipT_neqxT_compat :
   {m n} {M N : 'E^{m.+1,n.+1}} {i0 j0},
    neqxT M N i0 j0 skipT M i0 j0 skipT N i0 j0.
Proof.
move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply skipT_reg.
Qed.

Lemma skipT_neqxT_reg :
   {m n} {M N : 'E^{m.+1,n.+1}} {i0 j0},
    skipT M i0 j0 skipT N i0 j0 neqxT M N i0 j0.
Proof.
move=>>; rewrite contra_not_l_equiv -eqxT_not_equiv eqxT_equiv; easy.
Qed.

Lemma neqxTr_equiv :
   {m n} {M N : 'E^{m.+1,n}} {i0},
    neqxTr M N i0 skipTr M i0 skipTr N i0.
Proof. move=>>; apply neqxF_equiv. Qed.

Lemma neqxTc_equiv :
   {m n} {M N : 'E^{m,n.+1}} {j0},
    neqxTc M N j0 skipTc M j0 skipTc N j0.
Proof.
intros; split;
    [intros; apply skipTc_neqxTc_compat; easy | apply skipTc_neqxTc_reg].
Qed.

Lemma neqxT_equiv :
   {m n} {M N : 'E^{m.+1,n.+1}} {i0 j0},
    neqxT M N i0 j0 skipT M i0 j0 skipT N i0 j0.
Proof.
intros; split;
    [intros; apply skipT_neqxT_compat; easy | apply skipT_neqxT_reg].
Qed.

Lemma extT_skipTr :
   {m n} {M N : 'E^{m.+1,n}} i0,
    row M i0 = row N i0 skipTr M i0 = skipTr N i0 M = N.
Proof. move=>>; apply extF_skipF. Qed.

Lemma extT_skipTr_equiv :
   {m n} {M N : 'E^{m.+1,n}} i0,
    M = N row M i0 = row N i0 skipTr M i0 = skipTr N i0.
Proof.
intros m n M N i0; split; intros H; [subst | apply (extT_skipTr i0)]; easy.
Qed.

Lemma extT_skipTc :
   {m n} {M N : 'E^{m,n.+1}} j0,
    col M j0 = col N j0 skipTc M j0 = skipTc N j0 M = N.
Proof.
intros m n M N j0 H0 H1; apply flipT_inj, (extT_skipTr j0); try easy.
rewrite -2!flipT_skipTc; apply flipT_eq; easy.
Qed.

Lemma extT_skipTc_equiv :
   {m n} {M N : 'E^{m,n.+1}} j0,
    M = N col M j0 = col N j0 skipTc M j0 = skipTc N j0.
Proof.
intros m n M N j0; split; intros H; [subst | apply (extT_skipTc j0)]; easy.
Qed.

Lemma extT_skipT :
   {m n} {M N : 'E^{m.+1,n.+1}} i0 j0,
    row M i0 = row N i0 col M j0 = col N j0
    skipT M i0 j0 = skipT N i0 j0 M = N.
Proof.
intros m n M N i0 j0 H0i H0j H1.
apply (extT_skipTr i0); try easy.
apply (extT_skipTc j0); try easy.
apply extF; intros i; unfold col in ×.
rewrite 2!skipTr_correct; apply (extF_rev _ _ H0j (skip_ord i0 i)).
Qed.

Lemma extT_skipT_equiv :
   {m n} {M N : 'E^{m.+1,n.+1}} i0 j0,
    M = N
    row M i0 = row N i0 col M j0 = col N j0 skipT M i0 j0 = skipT N i0 j0.
Proof.
intros m n M N i0 j0; split; intros H; [subst | apply (extT_skipT i0 j0)]; easy.
Qed.

Lemma skipTc_castTr :
   {m1 m2 n} (Hm : m1 = m2) (M1 : 'E^{m1,n.+1}) j0,
    skipTc (castTr Hm M1) j0 = castTr Hm (skipTc M1 j0).
Proof. easy. Qed.

Lemma skipTr_castTc :
   {m n1 n2} (Hn : n1 = n2) (M1 : 'E^{m.+1,n1}) i0,
    skipTr (castTc Hn M1) i0 = castTc Hn (skipTr M1 i0).
Proof. easy. Qed.

Lemma skipTr_concatTr :
   {m n} (M : 'E^{m.+1,n}) i0,
    castTr (ord_split i0) (skipTr M i0) =
      concatTr (upT (castTr (ord_splitS i0) M))
               (downT (castTr (ordS_splitS i0) M)).
Proof. intros; apply skipF_concatF. Qed.

Lemma skipTc_concatTc :
   {m n} (M : 'E^{m,n.+1}) j0,
    castTc (ord_split j0) (skipTc M j0) =
      concatTc (leftT (castTc (ord_splitS j0) M))
               (rightT (castTc (ordS_splitS j0) M)).
Proof. intros; apply extF; intro; apply skipF_concatF. Qed.

Lemma skipT_concatT :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0,
    castT (ord_split i0) (ord_split j0) (skipT M i0 j0) =
      concatT (ulT (castT (ord_splitS i0) (ord_splitS j0) M))
              (urT (castT (ord_splitS i0) (ordS_splitS j0) M))
              (dlT (castT (ordS_splitS i0) (ord_splitS j0) M))
              (drT (castT (ordS_splitS i0) (ordS_splitS j0) M)).
Proof.
intros; unfold castT; rewrite -skipTr_castTc skipTr_concatTr.
apply flipT_inj; rewrite -concatTc_flipT -concatT_flipT concatT_equiv_def.
rewrite -leftT_flipT -ulT_flipT -dlT_flipT ulT_equiv_def dlT_equiv_def -leftT_concatTr.
rewrite -rightT_flipT -urT_flipT -drT_flipT urT_equiv_def drT_equiv_def -rightT_concatTr.
rewrite 6!flipT_castTr 3!flipT_castTc.
rewrite 2!upT_castTc 2!downT_castTc 2!concatTr_castTc flipT_skipTc.
rewrite skipTr_concatTr; easy.
Qed.

Lemma skipTr_insertTr :
   {m n} (M : 'E^{m,n}) A i0, skipTr (insertTr M A i0) i0 = M.
Proof. intros; apply skipF_insertF. Qed.

Lemma insertTr_skipTr :
   {m n} (M : 'E^{m.+1,n}) i0, insertTr (skipTr M i0) (row M i0) i0 = M.
Proof. intros; apply insertF_skipF. Qed.

Lemma skipTc_insertTc :
   {m n} (M : 'E^{m,n}) B j0, skipTc (insertTc M B j0) j0 = M.
Proof. intros; apply extF; intro; apply skipF_insertF. Qed.

Lemma insertTc_skipTc :
   {m n} (M : 'E^{m,n.+1}) j0, insertTc (skipTc M j0) (col M j0) j0 = M.
Proof.
intros; apply extF; intro; unfold insertTc; rewrite insertF_skipF; easy.
Qed.

Lemma skipT_insertT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    skipT (insertT M A B x i0 j0) i0 j0 = M.
Proof.
intros; unfold skipT; rewrite insertT_equiv_def skipTc_insertTc skipTr_insertTr; easy.
Qed.

Lemma insertT_skipT :
   {m n} (M : 'E^{m.+1,n.+1}) i0 j0,
    insertT (skipT M i0 j0) (row (skipTc M j0) i0)
      (col (skipTr M i0) j0) (M i0 j0) i0 j0 = M.
Proof.
intros; unfold insertT;
    rewrite skipT_equiv_def insertTc_skipTc insertF_skipF insertTr_skipTr; easy.
Qed.

Lemma skipTr_insertTc :
   {m n} (M : 'E^{m.+1,n}) B i0 j0,
    skipTr (insertTc M B j0) i0 = insertTc (skipTr M i0) (skipF B i0) j0.
Proof.
intros m n M B i0 j0; apply extT; intros i j.
destruct (lt_dec i i0), (ord_eq_dec j j0) as [Hj | Hj]; unfold skipTr.
rewriteinsertTc_correct_l, 2!skipF_correct_l; try easy.
unfold widenF_S; rewrite insertTc_correct_l; easy.
rewrite → (insertTc_correct_r _ _ _ Hj), 2!skipF_correct_l; try easy.
unfold widenF_S; rewrite insertTc_correct_r; easy.
rewriteinsertTc_correct_l, 2!skipF_correct_r; try easy.
unfold liftF_S; rewrite insertTc_correct_l; easy.
rewrite → (insertTc_correct_r _ _ _ Hj), 2!skipF_correct_r; try easy.
unfold liftF_S; rewrite insertTc_correct_r; easy.
Qed.

Lemma insertTc_skipTr :
   {m n} (M : 'E^{m.+1,n}) B x i0 j0,
    insertTc (skipTr M i0) B j0 = skipTr (insertTc M (insertF B x i0) j0) i0.
Proof. intros; rewrite skipTr_insertTc skipF_insertF; easy. Qed.

Lemma skipTc_insertTr :
   {m n} (M : 'E^{m,n.+1}) A i0 j0,
    skipTc (insertTr M A i0) j0 = insertTr (skipTc M j0) (skipF A j0) i0.
Proof.
intros; apply flipT_inj.
rewrite flipT_skipTc 2!flipT_insertTr flipT_skipTc skipTr_insertTc; easy.
Qed.

Lemma insertTr_skipTc :
   {m n} (M : 'E^{m,n.+1}) A x i0 j0,
    insertTr (skipTc M j0) A i0 = skipTc (insertTr M (insertF A x j0) i0) j0.
Proof. intros; rewrite skipTc_insertTr skipF_insertF; easy. Qed.

Lemma skipTr_ex :
   {m n} M0 (M1 : 'E^{m,n}) i0, M,
    row M i0 = M0 skipTr M i0 = M1.
Proof. intros; apply skipF_ex. Qed.

Lemma skipTc_ex :
   {m n} M0 (M1 : 'E^{m,n}) j0, M,
    col M j0 = M0 skipTc M j0 = M1.
Proof.
intros m n M0 M1 j0; destruct (skipTr_ex M0 (flipT M1) j0) as [M [HM1 HM2]].
(flipT M); split; try apply flipT_inj; easy.
Qed.

Lemma skipT_ex :
   {m n} Mi0j0 Mi0 Mj0 (M1 : 'E^{m,n}) i0 j0,
     M, M i0 j0 = Mi0j0
      skipF (row M i0) j0 = Mi0 skipF (col M j0) i0 = Mj0
      skipT M i0 j0 = M1.
Proof.
intros m n Mi0j0 Mi0 Mj0 M1 i0 j0.
destruct (skipTr_ex Mi0 M1 i0) as [M1' [HM1'a HM1'b]].
destruct (skipF_ex Mi0j0 Mj0 i0) as [Mj0' [HMj0'a HMj0'b]].
destruct (skipTc_ex Mj0' M1' j0) as [M [HMa HMb]].
M; repeat split.
rewrite -HMj0'a -HMa; easy.
rewrite -HM1'a -HMb; easy.
rewrite -HMj0'b -HMa; easy.
rewrite -HM1'b -HMb; easy.
Qed.

Lemma skipTr_uniq :
   {m n} M0 (M1 : 'E^{m,n}) i0,
    ! M, row M i0 = M0 skipTr M i0 = M1.
Proof. intros; apply skipF_uniq. Qed.

Lemma skipTc_uniq :
   {m n} M0 (M1 : 'E^{m,n}) j0,
    ! M, col M j0 = M0 skipTc M j0 = M1.
Proof.
intros m n M0 M1 j0; destruct (skipTr_uniq M0 (flipT M1) j0) as [M [HMa HMb]].
(flipT M); repeat split.
rewrite col_correct flipT_invol; easy.
apply flipT_inj; rewrite flipT_skipTc flipT_invol; easy.
intros N HN; rewrite -(flipT_invol N).
apply flipT_eq, (HMb (flipT N)); split; try easy.
rewrite -flipT_skipTc; apply flipT_eq; easy.
Qed.

Lemma skipT_uniq :
   {m n} Mi0j0 Mi0 Mj0 (M1 : 'E^{m,n}) i0 j0,
    ! M, M i0 j0 = Mi0j0
      skipF (row M i0) j0 = Mi0 skipF (col M j0) i0 = Mj0
      skipT M i0 j0 = M1.
Proof.
intros m n Mi0j0 Mi0 Mj0 M1 i0 j0.
destruct (skipT_ex Mi0j0 Mi0 Mj0 M1 i0 j0) as [M HM].
M; split; try easy.
intros N [HNi0j0 [HNi0 [HNj0 HN1]]]; apply (extT_skipT i0 j0).
apply (extF_skipF j0).
unfold row; rewrite HNi0j0; easy.
rewrite HNi0; easy.
apply (extF_skipF i0).
unfold col; rewrite HNi0j0; easy.
rewrite HNj0; easy.
rewrite HN1; easy.
Qed.

Properties of operators replaceTr/replaceTc/replaceT.

Lemma replaceTr_equiv_def_insertTr :
   {m n} (M : 'E^{m.+1,n}) A i0,
    replaceTr M A i0 = insertTr (skipTr M i0) A i0.
Proof. intros; apply replaceF_equiv_def_insertF. Qed.

Lemma replaceTr_equiv_def_skipTr :
   {m n} (M : 'E^{m,n}) A i0,
    replaceTr M A i0 = skipTr (insertTr M A (widen_S i0)) (lift_S i0).
Proof. intros; apply replaceF_equiv_def_skipF. Qed.

Lemma replaceTc_equiv_def_insertTc :
   {m n} (M : 'E^{m,n.+1}) B j0,
    replaceTc M B j0 = insertTc (skipTc M j0) B j0.
Proof. intros; apply extF; intro; apply replaceF_equiv_def_insertF. Qed.

Lemma replaceTc_equiv_def_skipTc :
   {m n} (M : 'E^{m,n}) B j0,
    replaceTc M B j0 = skipTc (insertTc M B (widen_S j0)) (lift_S j0).
Proof. intros; apply extF; intro; apply replaceF_equiv_def_skipF. Qed.

Lemma replaceT_equiv_def_insertT :
   {m n} (M : 'E^{m.+1,n.+1}) A B x i0 j0,
    replaceT M A B x i0 j0 =
      insertT (skipT M i0 j0) (skipF A j0) (skipF B i0) x i0 j0.
Proof.
intros; unfold replaceT.
rewrite replaceTr_equiv_def_insertTr replaceTc_equiv_def_insertTc replaceF_equiv_def_insertF skipTr_insertTc. easy.
Qed.

Lemma replaceT_equiv_def_skipT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    replaceT M A B x i0 j0 =
      skipT (insertT M A B x (widen_S i0) (widen_S j0)) (lift_S i0) (lift_S j0).
Proof.
intros; unfold replaceT, skipT.
rewrite replaceTr_equiv_def_skipTr replaceTc_equiv_def_skipTc replaceF_equiv_def_skipF
    skipTc_insertTr. easy.
Qed.

Lemma flipT_replaceTr :
   {m n} (M : 'E^{m,n}) A i0,
    flipT (replaceTr M A i0) = replaceTc (flipT M) A i0.
Proof.
intros; rewrite replaceTr_equiv_def_skipTr replaceTc_equiv_def_skipTc.
rewrite flipT_skipTr flipT_insertTr; easy.
Qed.

Lemma flipT_replaceTc :
   {m n} (M : 'E^{m,n}) B j0,
    flipT (replaceTc M B j0) = replaceTr (flipT M) B j0.
Proof. intros; apply flipT_inj; rewrite flipT_replaceTr; easy. Qed.

Lemma flipT_replaceT :
   {m n} (M : 'E^{m,n}) A B x i0 j0,
    flipT (replaceT M A B x i0 j0) = replaceT (flipT M) B A x j0 i0.
Proof. intros; rewrite replaceT_equiv_def flipT_replaceTc flipT_replaceTr; easy. Qed.

Lemma replaceTr_compat_gen :
   {m n} (M N : 'E^{m,n}) A C i0 k0,
    eqxTr M N i0 A = C i0 = k0 replaceTr M A i0 = replaceTr N C k0.
Proof. move=>>; apply replaceF_compat_gen. Qed.

Lemma replaceTc_compat_gen :
   {m n} (M N : 'E^{m,n}) B D j0 l0,
    eqxTc M N j0 B = D j0 = l0 replaceTc M B j0 = replaceTc N D l0.
Proof.
move=>> H HB Hj0; apply extF; intro.
apply replaceF_compat_gen; try rewrite HB; easy.
Qed.

Lemma replaceT_compat_gen :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0 k0 l0,
    eqxT M N i0 j0 eqxF A C j0 eqxF B D i0
    x = y i0 = k0 j0 = l0
    replaceT M A B x i0 j0 = replaceT N C D y k0 l0.
Proof.
intros m n M N A B C D x y i0 j0 k0 l0 HM HA HB Hx Hi0 Hj0;
    rewrite -Hx -Hi0 -Hj0.
apply extT; intros i j; destruct (ord_eq_dec i i0), (ord_eq_dec j j0).
1,2: rewrite → 2!replaceT_correct_lr,
    (replaceF_compat_gen _ C _ x _ j0); easy.
rewrite → 2!replaceT_correct_lc, (replaceF_compat_gen _ D _ x _ i0); easy.
rewrite → 2!replaceT_correct_r; auto.
Qed.

Lemma replaceTr_compat :
   {m n} (M N : 'E^{m,n}) A C i0,
    eqxTr M N i0 A = C replaceTr M A i0 = replaceTr N C i0.
Proof. intros; apply replaceTr_compat_gen; easy. Qed.

Lemma replaceTc_compat :
   {m n} (M N : 'E^{m,n}) B D j0 ,
    eqxTc M N j0 B = D replaceTc M B j0 = replaceTc N D j0.
Proof. intros; apply replaceTc_compat_gen; easy. Qed.

Lemma replaceT_compat :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    eqxT M N i0 j0 eqxF A C j0 eqxF B D i0 x = y
    replaceT M A B x i0 j0 = replaceT N C D y i0 j0.
Proof. intros; apply replaceT_compat_gen; easy. Qed.

Lemma replaceTr_reg_l :
   {m n} (M N : 'E^{m,n}) A C i0,
    replaceTr M A i0 = replaceTr N C i0 eqxTr M N i0.
Proof. move=>> H; eapply replaceF_reg_l; apply H. Qed.

Lemma replaceTr_reg_r :
   {m n} (M N : 'E^{m,n}) A C i0,
    replaceTr M A i0 = replaceTr N C i0 A = C.
Proof. move=>> H; eapply replaceF_reg_r; apply H. Qed.

Lemma replaceTr_reg :
   {m n} (M N : 'E^{m,n}) A C i0,
    replaceTr M A i0 = replaceTr N C i0 eqxTr M N i0 A = C.
Proof. move=>> H; eapply replaceF_reg; apply H. Qed.

Lemma replaceTc_reg_l :
   {m n} (M N : 'E^{m,n}) B D j0,
    replaceTc M B j0 = replaceTc N D j0 eqxTc M N j0.
Proof.
move=>> /flipT_eq; rewrite 2!flipT_replaceTc.
move⇒ /replaceTr_reg_l; apply eqxTr_flipT.
Qed.

Lemma replaceTc_reg_r :
   {m n} (M N : 'E^{m,n}) B D j0,
    replaceTc M B j0 = replaceTc N D j0 B = D.
Proof.
move=>> /flipT_eq; rewrite 2!flipT_replaceTc; apply replaceTr_reg_r.
Qed.

Lemma replaceTc_reg :
   {m n} (M N : 'E^{m,n}) B D j0,
    replaceTc M B j0 = replaceTc N D j0 eqxTc M N j0 B = D.
Proof.
move=>> H; split; [eapply replaceTc_reg_l | eapply replaceTc_reg_r]; apply H.
Qed.

Lemma replaceT_reg_l :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    replaceT M A B x i0 j0 = replaceT N C D y i0 j0 eqxT M N i0 j0.
Proof.
move=>> /extT_rev H i j Hi Hj; specialize (H i j); simpl in H.
erewrite 2!replaceT_correct_r in H; easy.
Qed.

Lemma replaceT_reg_ml :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    replaceT M A B x i0 j0 = replaceT N C D y i0 j0 eqxF A C j0.
Proof. move=>> /replaceTr_reg_r H; eapply replaceF_reg_l; apply H. Qed.

Lemma replaceT_reg_mr :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    replaceT M A B x i0 j0 = replaceT N C D y i0 j0 eqxF B D i0.
Proof.
move=>>; rewrite 2!replaceT_equiv_def.
move⇒ /replaceTc_reg_r H; eapply replaceF_reg_l; apply H.
Qed.

Lemma replaceT_reg_r :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    replaceT M A B x i0 j0 = replaceT N C D y i0 j0 x = y.
Proof. move=>> /replaceTr_reg_r H; eapply replaceF_reg_r; apply H. Qed.

Lemma replaceT_reg :
   {m n} (M N : 'E^{m,n}) A B C D x y i0 j0,
    replaceT M A B x i0 j0 = replaceT N C D y i0 j0
    eqxT M N i0 j0 eqxF A C j0 eqxF B D i0 x = y.
Proof.
move=>> H; repeat split;
    [eapply replaceT_reg_l | eapply replaceT_reg_ml |
     eapply replaceT_reg_mr | eapply replaceT_reg_r]; apply H.
Qed.

Lemma eqxTc_replaceTr :
   {m n} (M N : 'E^{m,n}) A C i0 k0 j0,
    eqxT M N i0 j0 A = C i0 = k0
    eqxTc (replaceTr M A i0) (replaceTr N C k0) j0.
Proof.
intros m n M N A C i0 k0 j0 HMN HAC Hik; rewrite -HAC -Hik.
intros i j Hj; destruct (ord_eq_dec i i0).
rewrite → 2!replaceTr_correct_l; easy.
rewrite → 2!replaceTr_correct_r; auto.
Qed.

Lemma eqxTr_replaceTc :
   {m n} (M N : 'E^{m,n}) B D j0 l0 i0,
    eqxT M N i0 j0 B = D j0 = l0
    eqxTr (replaceTc M B j0) (replaceTc N D l0) i0.
Proof.
intros m n M N B D j0 l0 i0 HMN HBD Hjl; rewrite -HBD -Hjl.
intros i Hi; apply extF; intros j; destruct (ord_eq_dec j j0).
rewrite → 2!replaceTc_correct_l; easy.
rewrite → 2!replaceTc_correct_r; auto.
Qed.

Lemma replaceTr_neqxTr_compat_l :
   {m n} {M N : 'E^{m,n}} A C {i0},
    neqxTr M N i0 replaceTr M A i0 replaceTr N C i0.
Proof. move=>>; apply replaceF_neqxF_compat_l. Qed.

Lemma replaceTr_neqxTr_compat_r :
   {m n} (M N : 'E^{m,n}) {A C} i0,
    A C replaceTr M A i0 replaceTr N C i0.
Proof. move=>>; apply replaceF_neqxF_compat_r. Qed.

Lemma replaceTr_neqxTr_reg :
   {m n} {M N : 'E^{m,n}} {A C i0},
    replaceTr M A i0 replaceTr N C i0 neqxTr M N i0 A C.
Proof. move=>>; apply replaceF_neqxF_reg. Qed.

Lemma replaceTr_neqxTr_equiv :
   {m n} {M N : 'E^{m,n}} {A C i0},
    replaceTr M A i0 replaceTr N C i0 neqxTr M N i0 A C.
Proof.
intros; split; [apply replaceTr_neqxTr_reg | intros [H | H]];
    [apply replaceTr_neqxTr_compat_l | apply replaceTr_neqxTr_compat_r]; easy.
Qed.

Lemma replaceTc_neqxTc_compat_l :
   {m n} {M N : 'E^{m,n}} B D {j0},
    neqxTc M N j0 replaceTc M B j0 replaceTc N D j0.
Proof.
move=>>; rewrite contra_not_r_equiv -eqxTc_not_equiv; apply replaceTc_reg.
Qed.

Lemma replaceTc_neqxTc_compat_r :
   {m n} {M N : 'E^{m,n}} {B D} j0,
    B D replaceTc M B j0 replaceTc N D j0.
Proof. move=>>; rewrite -contra_equiv; apply replaceTc_reg. Qed.

Lemma replaceTc_neqxTc_reg :
   {m n} {M N : 'E^{m,n}} {B D j0},
    replaceTc M B j0 replaceTc N D j0 neqxTc M N j0 B D.
Proof.
move=>>; rewrite neqxTc_not_equiv -not_and_equiv -contra_equiv.
intros; apply replaceTc_compat; easy.
Qed.

Lemma replaceTc_neqxTc_equiv :
   {m n} {M N : 'E^{m,n}} {B D j0},
    replaceTc M B j0 replaceTc N D j0 neqxTc M N j0 B D.
Proof.
intros; split; [apply replaceTc_neqxTc_reg | intros [H | H]];
    [apply replaceTc_neqxTc_compat_l | apply replaceTc_neqxTc_compat_r]; easy.
Qed.

Lemma replaceT_neqxT_compat_l :
   {m n} {M N : 'E^{m,n}} A B C D x y {i0 j0},
    neqxT M N i0 j0 replaceT M A B x i0 j0 replaceT N C D y i0 j0.
Proof.
move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply replaceT_reg.
Qed.

Lemma replaceT_neqxT_compat_ml :
   {m n} (M N : 'E^{m,n}) {A} B {C} D x y i0 {j0},
    neqxF A C j0 replaceT M A B x i0 j0 replaceT N C D y i0 j0.
Proof.
move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg.
Qed.

Lemma replaceT_neqxT_compat_mr :
   {m n} (M N : 'E^{m,n}) A {B} C {D} x y {i0} j0,
    neqxF B D i0 replaceT M A B x i0 j0 replaceT N C D y i0 j0.
Proof.
move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg.
Qed.

Lemma replaceT_neqxT_compat_r :
   {m n} (M N : 'E^{m,n}) A B C D {x y} i0 j0,
    x y replaceT M A B x i0 j0 replaceT N C D y i0 j0.
Proof. move=>>; rewrite -contra_equiv; apply replaceT_reg. Qed.

Lemma replaceT_neqxT_reg :
   {m n} {M N : 'E^{m,n}} {A B C D x y i0 j0},
    replaceT M A B x i0 j0 replaceT N C D y i0 j0
    neqxT M N i0 j0 neqxF A C j0 neqxF B D i0 x y.
Proof.
move=>>; rewrite neqxT_not_equiv 2!neqxF_not_equiv
    -not_and4_equiv -contra_equiv.
intros; apply replaceT_compat; easy.
Qed.

Lemma replaceT_neqxT_equiv :
   {m n} {M N : 'E^{m,n}} {A B C D x y i0 j0},
    replaceT M A B x i0 j0 replaceT N C D y i0 j0
    neqxT M N i0 j0 neqxF A C j0 neqxF B D i0 x y.
Proof.
intros; split; [apply replaceT_neqxT_reg | intros [H | [H | [H | H]]]];
    [apply replaceT_neqxT_compat_l | apply replaceT_neqxT_compat_ml |
     apply replaceT_neqxT_compat_mr | apply replaceT_neqxT_compat_r]; easy.
Qed.

Lemma replaceTr_constT :
   {m n} (x : E) i0,
    replaceTr (constT m n x) (constF n x) i0 = constT m n x.
Proof. intros; apply replaceF_constF. Qed.

Lemma replaceTc_constT :
   {m n} (x : E) j0,
    replaceTc (constT m n x) (constF m x) j0 = constT m n x.
Proof. intros; apply extF; intro; apply replaceF_constF. Qed.

Lemma replaceT_constT :
   {m n} (x : E) i0 j0,
    replaceT (constT m n x) (constF n x) (constF m x) x i0 j0 = constT m n x.
Proof.
intros; unfold replaceT; rewrite replaceTc_constT replaceF_constF.
apply replaceTr_constT.
Qed.

Lemma extTr_replaceTr :
   {m n} (M N : 'E^{m,n}) A i0,
    row M i0 = row N i0 replaceTr M A i0 = replaceTr N A i0 M = N.
Proof. move=>>; apply extF_replaceF. Qed.

Lemma extTc_replaceTc :
   {m n} (M N : 'E^{m,n}) B j0,
    col M j0 = col N j0 replaceTc M B j0 = replaceTc N B j0 M = N.
Proof.
movem n M N B j0 /extF_rev H0 H.
apply extT; intros i j; destruct (ord_eq_dec j j0) as [Hj | Hj].
unfold col in H0; rewrite Hj; easy.
rewrite -(replaceTc_correct_r M B i Hj)
    -(replaceTc_correct_r N B i Hj) H; easy.
Qed.

Lemma extT_replaceT :
   {m n} (M N : 'E^{m,n}) A B x i0 j0,
    row M i0 = row N i0 col M j0 = col N j0
    replaceT M A B x i0 j0 = replaceT N A B x i0 j0 M = N.
Proof.
movem n M N A B x i0 j0 /extF_rev Hi0 /extF_rev Hj0 H;
    unfold row in Hi0; unfold col in Hj0; apply extT; intros i j;
    destruct (ord_eq_dec i i0) as [Hi | Hi], (ord_eq_dec j j0) as [Hj | Hj];
    try rewrite Hi; try rewrite Hj; try easy.
rewrite -(replaceT_correct_r M A B x Hi Hj)
    -(replaceT_correct_r N A B x Hi Hj) H; easy.
Qed.

Lemma skipTr_replaceTr :
   {m n} (M : 'E^{m.+1,n}) A i0,
    skipTr (replaceTr M A i0) i0 = skipTr M i0.
Proof. intros; apply skipF_replaceF. Qed.

Lemma skipTc_replaceTc :
   {m n} (M : 'E^{m,n.+1}) B j0,
    skipTc (replaceTc M B j0) j0 = skipTc M j0.
Proof. intros; apply skipTc_compat; do 2 intro; apply replaceTc_correct_r. Qed.

Lemma skipT_replaceT :
   {m n} (M : 'E^{m.+1,n.+1}) A B x i0 j0,
    skipT (replaceT M A B x i0 j0) i0 j0 = skipT M i0 j0.
Proof. intros; apply skipT_compat; do 2 intro; apply replaceT_correct_r. Qed.

Properties of operator mapijT/mapT.

Context {F G : Type}.

Lemma mapT_comp :
   {m n} (f : E F) (g : F G) (M : 'E^{m,n}),
    mapT (g \o f) M = mapT g (mapT f M).
Proof. easy. Qed.

Lemma mapT_eq :
   {m n} (f : E F) (M N : 'E^{m,n}), M = N mapT f M = mapT f N.
Proof. intros; f_equal; easy. Qed.

Lemma mapT_inj :
   {m n} (f : E F) (M N : 'E^{m,n}),
    injective f mapT f M = mapT f N M = N.
Proof.
intros m n f M N Hf H.
apply (mapF_inj (mapF f)); try easy; f_equal.
intros A B; apply mapF_inj; easy.
Qed.

Lemma mapT_eq_f :
   {m n} (f g : E F) (M : 'E^{m,n}), f = g mapT f M = mapT g M.
Proof. intros; f_equal; easy. Qed.

Lemma mapT_inj_f :
   m n (f g : E F),
    ( (M : 'E^{m.+1,n.+1}), mapT f M = mapT g M) f = g.
Proof.
intros m n f g H; apply (mapF_inj_f n f g); intros A.
apply (f_equal (fun hh A)), (mapF_inj_f m); easy.
Qed.

Lemma mapT_constF :
   {m n} (f : E F) (x : E), mapT f (constT m n x) = constT m n (f x).
Proof. easy. Qed.

Lemma mapT_blk1 :
   (f : E F) (x00 : E), mapT f (blk1T x00) = blk1T (f x00).
Proof. easy. Qed.

Lemma mapT_blk2 :
   (f : E F) (x00 x01 x10 x11 : E),
    mapT f (blk2T x00 x01 x10 x11) = blk2T (f x00) (f x01) (f x10) (f x11).
Proof. intros; unfold mapT; rewrite 3!mapF_coupleF;easy. Qed.

Lemma mapT_castTr :
   {m1 m2 n} (Hm : m1 = m2) (f : E F) (M1 : 'E^{m1,n}),
    mapT f (castTr Hm M1) = castTr Hm (mapT f M1).
Proof. easy. Qed.

Lemma mapT_castTc :
   {m n1 n2} (Hn : n1 = n2) (f : E F) (M1 : 'E^{m,n1}),
    mapT f (castTc Hn M1) = castTc Hn (mapT f M1).
Proof. easy. Qed.

Lemma mapT_castT :
   {m1 m2 n1 n2} (Hm : m1 = m2) (Hn : n1 = n2)
      (f : E F) (M1 : 'E^{m1,n1}),
    mapT f (castT Hm Hn M1) = castT Hm Hn (mapT f M1).
Proof. easy. Qed.

Lemma mapT_row :
   {m n} (f : E F) (M : 'E^{m,n}),
    mapT f (row M) = row (mapT f M).
Proof. easy. Qed.

Lemma mapT_col :
   {m n} (f : E F) (M : 'E^{m,n}),
    mapT f (col M) = col (mapT f M).
Proof. easy. Qed.

Lemma mapT_flipT :
   {m n} (f : E F) (M : 'E^{m,n}),
    mapT f (flipT M) = flipT (mapT f M).
Proof. easy. Qed.

Lemma mapT_upT :
   {m1 m2 n} (f : E F) (M : 'E^{m1 + m2,n}),
    mapT f (upT M) = upT (mapT f M).
Proof. easy. Qed.

Lemma mapT_downT :
   {m1 m2 n} (f : E F) (M : 'E^{m1 + m2,n}),
    mapT f (downT M) = downT (mapT f M).
Proof. easy. Qed.

Lemma mapT_leftT :
   {m n1 n2} (f : E F) (M : 'E^{m,n1 + n2}),
    mapT f (leftT M) = leftT (mapT f M).
Proof. easy. Qed.

Lemma mapT_rightT :
   {m n1 n2} (f : E F) (M : 'E^{m,n1 + n2}),
    mapT f (rightT M) = rightT (mapT f M).
Proof. easy. Qed.

Lemma mapT_ulT :
   {m1 m2 n1 n2} (f : E F) (M : 'E^{m1 + m2,n1 + n2}),
    mapT f (ulT M) = ulT (mapT f M).
Proof. easy. Qed.

Lemma mapT_urT :
   {m1 m2 n1 n2} (f : E F) (M : 'E^{m1 + m2,n1 + n2}),
    mapT f (urT M) = urT (mapT f M).
Proof. easy. Qed.

Lemma mapT_dlT :
   {m1 m2 n1 n2} (f : E F) (M : 'E^{m1 + m2,n1 + n2}),
    mapT f (dlT M) = dlT (mapT f M).
Proof. easy. Qed.

Lemma mapT_drT :
   {m1 m2 n1 n2} (f : E F) (M : 'E^{m1 + m2,n1 + n2}),
    mapT f (drT M) = drT (mapT f M).
Proof. easy. Qed.

Lemma mapT_concatTr :
   {m1 m2 n} (f : E F) (M1 : 'E^{m1,n}) (M2 : 'E^{m2,n}),
    mapT f (concatTr M1 M2) = concatTr (mapT f M1) (mapT f M2).
Proof. intros; apply mapF_concatF. Qed.

Lemma mapT_concatTc :
   {m n1 n2} (f : E F) (M1 : 'E^{m,n1}) (M2 : 'E^{m,n2}),
    mapT f (concatTc M1 M2) = concatTc (mapT f M1) (mapT f M2).
Proof. intros; apply extF; intro; apply mapF_concatF. Qed.

Lemma mapT_concatT :
   {m1 m2 n1 n2} (f : E F)
      (M11 : 'E^{m1,n1}) (M12 : 'E^{m1,n2}) (M21 : 'E^{m2,n1}) (M22 : 'E^{m2,n2}),
    mapT f (concatT M11 M12 M21 M22) =
      concatT (mapT f M11) (mapT f M12) (mapT f M21) (mapT f M22).
Proof. intros; rewrite mapT_concatTr 2!mapT_concatTc; easy. Qed.

Lemma mapT_insertTr :
   {m n} (f : E F) (M : 'E^{m,n}) A i0,
    mapT f (insertTr M A i0) = insertTr (mapT f M) (mapF f A) i0.
Proof. intros; unfold mapT; rewrite mapF_insertF; easy. Qed.

Lemma mapT_insertTc :
   {m n} (f : E F) (M : 'E^{m,n}) B j0,
    mapT f (insertTc M B j0) = insertTc (mapT f M) (mapF f B) j0.
Proof.
intros; apply extF; intro; unfold mapT, insertTc.
rewrite mapF_correct mapF_insertF; easy.
Qed.

Lemma mapT_insertT :
   {m n} (f : E F) (M : 'E^{m,n}) A B x i0 j0,
    mapT f (insertT M A B x i0 j0) =
      insertT (mapT f M) (mapF f A) (mapF f B) (f x) i0 j0.
Proof. intros; rewrite mapT_insertTr mapT_insertTc mapF_insertF; easy. Qed.

Lemma mapT_skipTr :
   {m n} (f : E F) (M : 'E^{m.+1,n}) i0,
    mapT f (skipTr M i0) = skipTr (mapT f M) i0.
Proof. easy. Qed.

Lemma mapT_skipTc :
   {m n} (f : E F) (M : 'E^{m,n.+1}) j0,
    mapT f (skipTc M j0) = skipTc (mapT f M) j0.
Proof. easy. Qed.

Lemma mapT_skipT :
   {m n} (f : E F) (M : 'E^{m.+1,n.+1}) i0 j0,
    mapT f (skipT M i0 j0) = skipT (mapT f M) i0 j0.
Proof. easy. Qed.

Lemma mapT_replaceTr :
   {m n} (f : E F) (M : 'E^{m,n}) A i0,
    mapT f (replaceTr M A i0) = replaceTr (mapT f M) (mapF f A) i0.
Proof. intros; unfold mapT; rewrite mapF_replaceF; easy. Qed.

Lemma mapT_replaceTc :
   {m n} (f : E F) (M : 'E^{m,n}) B j0,
    mapT f (replaceTc M B j0) = replaceTc (mapT f M) (mapF f B) j0.
Proof.
intros; apply extF; intro; unfold mapT, replaceTc.
rewrite mapF_correct mapF_replaceF; easy.
Qed.

Lemma mapT_replaceT :
   {m n} (f : E F) (M : 'E^{m,n}) A B x i0 j0,
    mapT f (replaceT M A B x i0 j0) =
      replaceT (mapT f M) (mapF f A) (mapF f B) (f x) i0 j0.
Proof. intros; rewrite mapT_replaceTr mapT_replaceTc mapF_replaceF; easy. Qed.

End FT_ops_Facts1.