Module definitions_typesCC2

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype fingroup.
Require Import finset zmodp ssralg perm advf_type seqmatrixCR matrix triangular_rs boolF2.


Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.


Section definitions.

Local Open Scope ring_scope.


Definition is_chaincomplex (M1 M2: matZ2) (m n n2: nat):=
  is_matrix m n M1 /\
  is_matrix n n2 M2 /\
  (mx_of_seqmx m n M1) *m (mx_of_seqmx n n2 M2) = 0.

Record chaincomplex:=
  {M1: matZ2;
   M2: matZ2;
   m: nat;
   n: nat;
   n2: nat;
   chaincomplex_proof: is_chaincomplex M1 M2 m n n2}.


Definition is_chaincomplex_morphism cc1 cc2 p1 p2 p3:=
  ((p1 *m (mx_of_seqmx (m cc1) (n cc1)(M1 cc1))) = ((mx_of_seqmx (m cc2) (n cc2)(M1 cc2))) *m p2) /\
  (p2 *m (mx_of_seqmx (n cc1) (n2 cc1)(M2 cc1)) = ((mx_of_seqmx (n cc2) (n2 cc2)(M2 cc2)) *m p3)).


Record chaincomplex_morphism (cc1 cc2: chaincomplex):=
  {p1: 'M['F_2]_(m cc2, m cc1);
   p2: 'M['F_2]_(n cc2, n cc1);
   p3: 'M['F_2]_(n2 cc2, n2 cc1);
   chaincomplex_morphism_proof: is_chaincomplex_morphism p1 p2 p3
}.


Record homotopy_op (cc1: chaincomplex):=
  {h1: 'M['F_2]_(n cc1, m cc1);
   h2: 'M['F_2]_(n2 cc1, n cc1)}.


Definition is_reduction_CC2 cc1 cc2 (f:chaincomplex_morphism cc1 cc2) (g:chaincomplex_morphism cc2 cc1)
   (h: homotopy_op cc1) :=
  (p1 f) *m (p1 g) = (1:'F_2)%:M /\
  (p2 f) *m (p2 g) = (1:'F_2)%:M /\
  (p3 f) *m (p3 g) = (1:'F_2)%:M /\
  (p1 g) *m (p1 f) + (mx_of_seqmx (m cc1) (n cc1) (M1 cc1)) *m (h1 h) = (1:'F_2)%:M /\
  (p2 g) *m (p2 f) + (mx_of_seqmx (n cc1) (n2 cc1) (M2 cc1)) *m (h2 h) +
     (h1 h) *m (mx_of_seqmx (m cc1) (n cc1) (M1 cc1)) = (1:'F_2)%:M /\
  (p3 g) *m (p3 f) + (h2 h) *m (mx_of_seqmx (n cc1) (n2 cc1) (M2 cc1)) = (1:'F_2)%:M /\
  (p2 f) *m (h1 h) = 0 /\
  (p3 f) *m (h2 h) = 0 /\
  (h1 h) *m (p1 g) = 0 /\
  (h2 h) *m (p2 g) = 0 /\
  (h2 h) *m (h1 h) = 0.


Record reduction_CC2 (cc1 cc2: chaincomplex):=
 {f: chaincomplex_morphism cc1 cc2;
  g: chaincomplex_morphism cc2 cc1;
  h: homotopy_op cc1;
  is_reduction_CC2_proof: is_reduction_CC2 f g h
  }.



Definition is_equivalence_CC2 cc1 cc2 (f:chaincomplex_morphism cc1 cc2) (g:chaincomplex_morphism cc2 cc1) :=
  (p1 f) *m (p1 g) = (1:'F_2)%:M /\
  (p1 g) *m (p1 f) = (1:'F_2)%:M /\
  (p2 f) *m (p2 g) = (1:'F_2)%:M /\
  (p2 g) *m (p2 f) = (1:'F_2)%:M /\
  (p3 f) *m (p3 g) = (1:'F_2)%:M /\
  (p3 g) *m (p3 f) = (1:'F_2)%:M.


Record equivalence_CC2 (cc1 cc2: chaincomplex):=
 {f_eq: chaincomplex_morphism cc1 cc2;
  g_eq: chaincomplex_morphism cc2 cc1;
  is_equivalence_CC2_proof: is_equivalence_CC2 f_eq g_eq
  }.


End definitions.



Section red_red_is_red_general.

Variables c c1 c2:chaincomplex.

Variable reduct_eq : reduction_CC2 c c1.

Variable reduct : reduction_CC2 c1 c2.

Local Open Scope ring_scope.

Definition f1'' := (p1 (f reduct)) *m (p1( f (reduct_eq))).
Definition f2'' := (p2 (f reduct)) *m (p2( f (reduct_eq))).
Definition f3'' := (p3 (f reduct)) *m (p3( f (reduct_eq))).
Definition g1'' := (p1 (g (reduct_eq))) *m (p1 (g reduct)).
Definition g2'' := (p2 (g (reduct_eq))) *m (p2 (g reduct)).
Definition g3'' := (p3 (g (reduct_eq))) *m (p3 (g reduct)).
Definition h1'' := (h1 (h reduct_eq)) + (p2 (g (reduct_eq)))*m (h1 (h reduct)) *m (p1 (f reduct_eq)).
Definition h2'' := (h2 (h reduct_eq)) + (p3 (g (reduct_eq)))*m (h2 (h reduct)) *m (p2 (f reduct_eq)).


Lemma f''_chaincomplex_morphism:
  (is_chaincomplex_morphism f1'' f2'' f3'').
Proof.
rewrite /is_chaincomplex_morphism /=.
move: (chaincomplex_morphism_proof (f reduct_eq)); rewrite /=; move =>[L1 L2].
move: (chaincomplex_morphism_proof (f reduct)); rewrite /=; move =>[L11 L21].
split; first by rewrite /f1'' /f2'' -mulmxA L1 !mulmxA L11.
by rewrite /f2'' /f3'' -mulmxA L2 !mulmxA L21.
Qed.


Definition chaincomplex_morphism_f'' := Build_chaincomplex_morphism f''_chaincomplex_morphism.


Lemma g''_chaincomplex_morphism:
  (is_chaincomplex_morphism g1'' g2'' g3'').
Proof.
rewrite /is_chaincomplex_morphism /=.
move: (chaincomplex_morphism_proof (g reduct_eq)); rewrite /=; move =>[L3 L4].
move: (chaincomplex_morphism_proof (g reduct)); rewrite /=; move =>[L31 L41].
split; first by rewrite /g1'' /g2'' -mulmxA L31 !mulmxA L3.
by rewrite /g1'' /g2'' -mulmxA L41 !mulmxA L4.
Qed.


Definition chaincomplex_morphism_g'' := Build_chaincomplex_morphism g''_chaincomplex_morphism.


Definition homotopy_op_h'' := (Build_homotopy_op h1'' h2'').


Lemma addmx_oppmx k l (A:'M['F_2]_(k, l)): addmx A (- A) = 0.
Proof.
have ->: (- A = oppmx A); first by done.
apply/matrixP => i j; rewrite !mxE.
by apply/eqP; rewrite GRing.subr_eq0.
Qed.

Lemma addmx_oppmx1 k l (A:'M['F_2]_(k, l)): addmx A (oppmx A) = 0.
Proof.
apply/matrixP => i j; rewrite !mxE.
by apply/eqP; rewrite GRing.subr_eq0.
Qed.


Lemma is_reduction_red_red: is_reduction_CC2 chaincomplex_morphism_f'' chaincomplex_morphism_g'' homotopy_op_h''.
Proof.
move: (chaincomplex_morphism_proof (f reduct_eq)); rewrite /=; move =>[L1 L2].
move: (chaincomplex_morphism_proof (g reduct_eq)); rewrite /=; move =>[L3 L4].
rewrite /is_reduction_CC2 /is_chaincomplex_morphism /=.
move: (is_reduction_CC2_proof reduct_eq)=>[H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 H111]]]]]]]]]].
move: (is_reduction_CC2_proof reduct)=>[H11 [H21 [H31 [H41 [H51 [H61 [H71 [H81 [H91 [H101 H102]]]]]]]]]].
split.
  rewrite /f1'' /g1''. rewrite mulmxA.
  by rewrite -(mulmxA (p1 (f reduct)) (p1 (f reduct_eq)) (p1 (g reduct_eq))) H1 mulmx1 H11.
split.
  rewrite /f2'' /g2''. rewrite mulmxA.
  by rewrite -(mulmxA (p2 (f reduct)) (p2 (f reduct_eq)) (p2 (g reduct_eq))) H2 mulmx1 H21.
split.
  rewrite /f3'' /g3''. rewrite mulmxA.
  by rewrite -(mulmxA (p3 (f reduct)) (p3 (f reduct_eq)) (p3 (g reduct_eq))) H3 mulmx1 H31.
split.
 rewrite /g1'' /f1'' /h1''.
 rewrite !mulmxA.
 rewrite -(mulmxA (p1 (g reduct_eq)) (p1 (g reduct)) (p1 (f reduct))).
 have ->: (p1 (g reduct) *m (p1 (f reduct)) = 1%:M - mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct)).
   have H201: addmx (addmx (p1 (g reduct) *m p1 (f reduct))
      (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct)))
      (oppmx (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct))) =
      1%:M + (oppmx (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct))).
      have H66: (addmx (p1 (g reduct) *m p1 (f reduct))
        ( (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct)))) = (p1 (g reduct) *m p1 (f reduct) +
         (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct))); first by rewrite /=.
      rewrite -H66 in H41.
      by rewrite H41.
   move: H201; rewrite -addmxA.
   by rewrite addmx_oppmx1 addmxC add0mx.
 have ->: ((1%:M - mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct)) =
       (1%:M + oppmx (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct)))); first by done.
 rewrite mulmxDr mulmxDl mulmx1.
  have ->: p1 (g reduct_eq) *m p1 (f reduct_eq) = 1%:M + oppmx (mx_of_seqmx (m c) (n c) (M1 c) *m h1 (h reduct_eq)).
   have H20: addmx (addmx (p1 (g reduct_eq) *m p1 (f reduct_eq))
      (mx_of_seqmx (m c) (n c) (M1 c) *m h1 (h reduct_eq)))
      (oppmx (mx_of_seqmx (m c) (n c) (M1 c) *m h1 (h reduct_eq))) =
      1%:M + (oppmx (mx_of_seqmx (m c) (n c) (M1 c) *m h1 (h reduct_eq))).
      have H66: (addmx (p1 (g reduct_eq) *m p1 (f reduct_eq))
        ( (mx_of_seqmx (m c) (n c) (M1 c) *m h1 (h reduct_eq)))) = (p1 (g reduct_eq) *m p1 (f reduct_eq) +
        (mx_of_seqmx (m c) (n c) (M1 c) *m h1 (h reduct_eq))); first by rewrite /=.
      rewrite -H66 in H4.
      by rewrite H4.
    move: H20; rewrite -addmxA.
    by rewrite addmx_oppmx1 addmxC add0mx.
  rewrite mulmxDr.
  set x:= (mx_of_seqmx (m c) (n c) (M1 c) *m h1 (h reduct_eq)).
  have <-: (addmx (1%:M + oppmx x + p1 (g reduct_eq) *m oppmx
        (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct)) *m p1 (f reduct_eq))
        ((x + mx_of_seqmx (m c) (n c) (M1 c) *m (p2 (g reduct_eq) *m h1 (h reduct) *m
                                    p1 (f reduct_eq))))) = 1%:M + oppmx x +
        p1 (g reduct_eq) *m oppmx (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1 (h reduct)) *m
        p1 (f reduct_eq) + (x + mx_of_seqmx (m c) (n c) (M1 c) *m (p2 (g reduct_eq) *m h1 (h reduct) *m
                                    p1 (f reduct_eq))); first by done.
  rewrite addmxC !addmxA -(addmxC (oppmx x)) -!addmxA !addmxA.
  rewrite -(addmxC x) addmx_oppmx1 add0mx -(addmxC 1%:M). rewrite -!addmxA.
  have ->:( (addmx (mx_of_seqmx (m c) (n c) (M1 c) *m (p2 (g reduct_eq) *m h1 (h reduct) *m
     p1 (f reduct_eq)))(p1 (g reduct_eq) *m oppmx (mx_of_seqmx (m c1) (n c1) (M1 c1) *m h1
      (h reduct)) *m p1 (f reduct_eq)))) = 0; last first.
    by rewrite addmxC add0mx.
  rewrite mulmxN.
  rewrite !mulmxA.
  rewrite -L3.
  by rewrite mulNmx addmx_oppmx.
split. rewrite /g2'' /f2'' /h2'' /h1''.
  rewrite mulmxA.
  set g2_eq:=p2 (g reduct_eq).
  set g2:= p2 (g reduct).
  set f2_eq:=p2 (f reduct_eq).
  set f2:= p2 (f reduct).
  set h2_eq:= h2 (h reduct_eq).
  set h2:= h2 (h reduct).
  set h1_eq:= h1 (h reduct_eq).
  set h1:= h1 (h reduct).
  set M2c:= mx_of_seqmx (n c) (n2 c) (M2 c).
  set M1c:= mx_of_seqmx (m c) (n c) (M1 c).
  set g3_eq:=p3 (g reduct_eq).
  set f1_eq:=p1 (f reduct_eq).
  rewrite -(mulmxA g2_eq g2 f2).
  have ->: (g2 *m f2) = 1%:M + (oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2)) + (oppmx (h1 *m (mx_of_seqmx (m c1) (n c1) (M1 c1)))).
    rewrite -/g2 -/f2 -/h2 -/h1 in H51.
    have H60:(g2 *m f2 + (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) +
      (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1))) + (oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)))
      = 1%:M + (oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1))); last first.
    move:H60.
    have ->:(g2 *m f2 + mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2 +
      h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1) +
      oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1))) =
      (addmx (g2 *m f2 + mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2 +
      h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) (oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)))); first by done.
    rewrite addmxC.
    have ->:((g2 *m f2 + mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2 +
   h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) =
         (addmx (g2 *m f2 + mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)))); first by done.
    rewrite -(addmxC (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1))).
    rewrite !addmxA. rewrite - (addmxC (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1))).
    rewrite addmx_oppmx1 add0mx.
    move=> H60.
    have H66: (addmx (g2 *m f2)(mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2)) +
     (oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2)) = 1%:M + oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1))
     + (oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2)).
      by rewrite H60.
    move: H66.
    have ->:(addmx (g2 *m f2) (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) + oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) =
              addmx (addmx (g2 *m f2) (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2))(oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2))); first by done.
    rewrite -addmxA addmx_oppmx addmxC add0mx.
    have ->:(1%:M + oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) +
      oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2)) =
      (addmx (addmx 1%:M (oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1))))(oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2))); first by done.
      rewrite -addmxA.
      rewrite (addmxC (oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)))).
      by rewrite addmxA.
    by rewrite H51.
  rewrite mulmxDr mulmxDr mulmx1.
  rewrite mulmxDl mulmxDl.
  have ->: (g2_eq *m f2_eq = 1%:M + (oppmx (M2c *m h2_eq)) + (oppmx (h1_eq *m M1c))).
    rewrite -/g2_eq -/f2_eq -/M2c -/M1c -/h2_eq -/h1_eq in H5.
    have H60:(g2_eq *m f2_eq + M2c *m h2_eq + h1_eq *m M1c) + (oppmx (h1_eq *m M1c)) = 1%:M + (oppmx (h1_eq *m M1c)); last first.
    move:H60.
    have ->:(g2_eq *m f2_eq + M2c *m h2_eq + h1_eq *m M1c + oppmx (h1_eq *m M1c)) =
       (addmx (g2_eq *m f2_eq + M2c *m h2_eq + h1_eq *m M1c) (oppmx (h1_eq *m M1c))); first by done.
    rewrite addmxC.
    have ->:((g2_eq *m f2_eq + M2c *m h2_eq + h1_eq *m M1c) =
         (addmx (g2_eq *m f2_eq + M2c *m h2_eq) (h1_eq *m M1c))); first by done.
    rewrite -(addmxC ((h1_eq *m M1c))).
    rewrite !addmxA. rewrite - (addmxC (h1_eq *m M1c)).
    rewrite addmx_oppmx1 add0mx.
    move=> H60.
    have H66: (addmx (g2_eq *m f2_eq) (M2c *m h2_eq)) + (oppmx (M2c *m h2_eq)) = 1%:M + oppmx (h1_eq *m M1c) + (oppmx (M2c *m h2_eq)).
      by rewrite H60.
    move: H66.
    have ->:(addmx (g2_eq *m f2_eq) (M2c *m h2_eq) + oppmx (M2c *m h2_eq) =
              addmx (addmx (g2_eq *m f2_eq) (M2c *m h2_eq))(oppmx (M2c *m h2_eq))); first by done.
    rewrite -addmxA addmx_oppmx addmxC add0mx.
    have ->:(1%:M + oppmx (h1_eq *m M1c) + oppmx (M2c *m h2_eq)) =
            (addmx (addmx 1%:M (oppmx (h1_eq *m M1c)))(oppmx (M2c *m h2_eq))); first by done.
      rewrite -addmxA.
      rewrite (addmxC (oppmx (h1_eq *m M1c))).
      by rewrite addmxA.
    by rewrite H5.
  rewrite mulmxDr.
  rewrite mulmxDl.
  have ->: (1%:M + oppmx (M2c *m h2_eq)) = addmx 1%:M (oppmx (M2c *m h2_eq)); first by done.
  rewrite addmxC.
  have ->: (addmx (oppmx (M2c *m h2_eq)) 1%:M + oppmx (h1_eq *m M1c) +
  g2_eq *m oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) *m f2_eq +
  g2_eq *m oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) *m f2_eq +
  (M2c *m h2_eq + M2c *m (g3_eq *m h2 *m f2_eq))) = addmx ((addmx (oppmx (M2c *m h2_eq)) 1%:M + oppmx (h1_eq *m M1c) +
  g2_eq *m oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) *m f2_eq +
  g2_eq *m oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) *m f2_eq))(M2c *m h2_eq + M2c *m (g3_eq *m h2 *m f2_eq)); first by done.
  rewrite addmxC.
  have ->: (M2c *m h2_eq + M2c *m (g3_eq *m h2 *m f2_eq)) = addmx (M2c *m h2_eq)(M2c *m (g3_eq *m h2 *m f2_eq)); first by done.
  rewrite -addmxA.
  rewrite (addmxC (M2c *m (g3_eq *m h2 *m f2_eq))).
 
  rewrite !addmxA.
  rewrite addmx_oppmx1 add0mx.
  rewrite -!addmxA.
  rewrite addmxA. rewrite (addmxC 1%:M).
  have ->:addmx (addmx (oppmx (h1_eq *m M1c)) 1%:M)
  (addmx (g2_eq *m oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) *m f2_eq)
  (addmx (g2_eq *m oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) *m f2_eq)
   (M2c *m (g3_eq *m h2 *m f2_eq)))) + (h1_eq *m M1c + g2_eq *m h1 *m f1_eq *m M1c) =
  addmx (addmx (addmx (oppmx (h1_eq *m M1c)) 1%:M)
  (addmx (g2_eq *m oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) *m f2_eq)
  (addmx (g2_eq *m oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) *m f2_eq)
  (M2c *m (g3_eq *m h2 *m f2_eq)))))((h1_eq *m M1c + g2_eq *m h1 *m f1_eq *m M1c)); first by done.
  rewrite addmxC.
  have ->: ((h1_eq *m M1c + g2_eq *m h1 *m f1_eq *m M1c) = addmx (h1_eq *m M1c)(g2_eq *m h1 *m f1_eq *m M1c)); first by done.
  rewrite (addmxC (h1_eq *m M1c)).
  rewrite -!addmxA.
  rewrite (addmxC (g2_eq *m h1 *m f1_eq *m M1c)).
  rewrite !addmxA.
  rewrite addmx_oppmx1 add0mx. rewrite -!addmxA.
  have ->:((addmx (g2_eq *m oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2) *m f2_eq)
    (addmx (g2_eq *m oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) *m f2_eq)
    (addmx (M2c *m (g3_eq *m h2 *m f2_eq)) (g2_eq *m h1 *m f1_eq *m M1c)))))= 0; last first.
    by rewrite addmxC add0mx.
  rewrite (addmxC (M2c *m (g3_eq *m h2 *m f2_eq))) addmxC !addmxA.
   have ->:(addmx (g2_eq *m oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) *m f2_eq)
      (g2_eq *m h1 *m f1_eq *m M1c))= 0.
     rewrite -(mulmxA (g2_eq *m h1)).
     rewrite L1.
     rewrite addmxC /f2_eq.
     have ->: oppmx (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)) =
              - (h1 *m mx_of_seqmx (m c1) (n c1) (M1 c1)); first by done.
     by rewrite mulmxN mulmxA mulNmx mulmxA addmx_oppmx.
  rewrite add0mx mulmxA mulmxA -L4 /g2_eq.
  have ->: (oppmx (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2)) =
            - (mx_of_seqmx (n c1) (n2 c1) (M2 c1) *m h2); first by done.
  by rewrite mulmxN mulmxA mulNmx addmx_oppmx.

split.
 rewrite /g3'' /f3'' /h2''.
 rewrite !mulmxA.
 rewrite -(mulmxA (p3 (g reduct_eq)) (p3 (g reduct)) (p3 (f reduct))).
 have ->: (p3 (g reduct) *m (p3 (f reduct)) = 1%:M - h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1)).
   have H201: addmx (addmx (p3 (g reduct) *m p3 (f reduct))
      (h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1)))
      (oppmx ( h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1))) =
      1%:M + (oppmx ( h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1))).
      have H66: (addmx (p3 (g reduct) *m p3 (f reduct))
        (h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1))) = (p3 (g reduct) *m p3 (f reduct) +
        h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1)); first by rewrite /=.
    rewrite -H66 in H61.
    by rewrite H61.
  move: H201; rewrite -addmxA.
  by rewrite addmx_oppmx1 addmxC add0mx.
  have ->: ((1%:M - h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1)) =
       (1%:M + oppmx ( h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1)))); first by done.
  rewrite mulmxDr mulmxDl mulmx1 mulmxDl.
  have ->: p3 (g reduct_eq) *m p3 (f reduct_eq) = 1%:M + oppmx (h2 (h reduct_eq) *m mx_of_seqmx (n c) (n2 c) (M2 c)).
    have H20: addmx (addmx (p3 (g reduct_eq) *m p3 (f reduct_eq))
      (h2 (h reduct_eq) *m mx_of_seqmx (n c) (n2 c) (M2 c)))
      (oppmx ( h2 (h reduct_eq) *m mx_of_seqmx (n c) (n2 c) (M2 c))) =
      1%:M + (oppmx ( h2 (h reduct_eq) *m mx_of_seqmx (n c) (n2 c) (M2 c))).
      have H66: (addmx (p3 (g reduct_eq) *m p3 (f reduct_eq))
        (h2 (h reduct_eq) *m mx_of_seqmx (n c) (n2 c) (M2 c))) = (p3 (g reduct_eq) *m p3 (f reduct_eq) +
        h2 (h reduct_eq) *m mx_of_seqmx (n c) (n2 c) (M2 c)); first by rewrite /=.
    rewrite -H66 in H6.
    by rewrite H6.
  move: H20; rewrite -addmxA.
  by rewrite addmx_oppmx1 addmxC add0mx.
  set x:= ((h2 (h reduct_eq)) *m (mx_of_seqmx (n c) (n2 c) (M2 c))).
  have <-: (addmx (1%:M + oppmx x + p3 (g reduct_eq) *m oppmx
        (h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1)) *m p3 (f reduct_eq))
        ((x + p3 (g reduct_eq) *m h2 (h reduct) *m p2 (f reduct_eq) *m mx_of_seqmx
        (n c) (n2 c) (M2 c)))) = 1%:M + oppmx x +
        p3 (g reduct_eq) *m oppmx (h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1) (M2 c1)) *m
        p3 (f reduct_eq) + (x + p3 (g reduct_eq) *m h2 (h reduct) *m p2 (f reduct_eq) *m
        mx_of_seqmx (n c) (n2 c) (M2 c)); first by done.
  rewrite addmxC !addmxA -(addmxC (oppmx x)) -!addmxA !addmxA.
  rewrite -(addmxC x) addmx_oppmx1 add0mx -(addmxC 1%:M). rewrite -!addmxA.
  have ->: ((addmx (p3 (g reduct_eq) *m h2 (h reduct) *m p2 (f reduct_eq) *m mx_of_seqmx
            (n c) (n2 c) (M2 c)) (p3 (g reduct_eq) *m oppmx
            (h2 (h reduct) *m mx_of_seqmx (n c1) (n2 c1)
            (M2 c1)) *m p3 (f reduct_eq))) = 0).
    rewrite mulmxN.
    rewrite -(mulmxA (p3 (g reduct_eq) *m h2 (h reduct)) (p2 (f reduct_eq))
         (mx_of_seqmx (n c) (n2 c) (M2 c))).
    by rewrite L2 !mulmxA mulNmx addmx_oppmx.
  by rewrite addmxC add0mx.
split. rewrite /f2'' /h1''.
  rewrite mulmxDr.
  rewrite -mulmxA H7 mulmx0.
  rewrite mulmxA mulmxA.
  rewrite -(mulmxA (p2 (f reduct))(p2 (f reduct_eq)) (p2 (g reduct_eq))).
  rewrite H2 mulmx1 H71 mul0mx.
  have ->: (0 + 0 = (addmx 0 0)); first by done.
  by rewrite add0mx.
split. rewrite /f3'' /h2''.
  rewrite mulmxDr -mulmxA H8 mulmx0 mulmxA mulmxA.
  rewrite -(mulmxA (p3 (f reduct))(p3 (f reduct_eq)) (p3 (g reduct_eq))).
  rewrite H3 mulmx1 H81 mul0mx.
  have ->: (0 + 0 = (addmx 0 0)); first by done.
  by rewrite add0mx.
split.
  rewrite /h1'' /g1''.
  rewrite mulmxDl. rewrite mulmxA H9 mul0mx.
  rewrite mulmxA.
  rewrite -(mulmxA (p2 (g reduct_eq) *m h1 (h reduct))(p1 (f reduct_eq))(p1 (g reduct_eq))).
  rewrite H1 mulmx1 -mulmxA H91 mulmx0.
  by have ->: (0 + 0 = (addmx 0 0)); last by rewrite add0mx.
split.
  rewrite /h2'' /g2''.
  rewrite mulmxDl. rewrite mulmxA H10 mul0mx.
  rewrite mulmxA.
  rewrite -(mulmxA (p3 (g reduct_eq) *m h2 (h reduct))(p2 (f reduct_eq))(p2 (g reduct_eq))).
  rewrite H2 mulmx1 -mulmxA H101 mulmx0.
  by have ->: (0 + 0 = (addmx 0 0)); last by rewrite add0mx.
rewrite /h2'' /h1''.
rewrite mulmxDl mulmxDr H111.
rewrite mulmxA mulmxA H10 !mul0mx mulmxDr.
rewrite -(mulmxA (p3 (g reduct_eq) *m h2 (h reduct)) (p2 (f reduct_eq))(h1 (h reduct_eq))).
rewrite H7 mulmx0 !mulmxA.
rewrite -(mulmxA (p3 (g reduct_eq) *m h2 (h reduct)) (p2 (f reduct_eq)) (p2 (g reduct_eq))).
rewrite H2 mulmx1 -(mulmxA (p3 (g reduct_eq)) (h2 (h reduct)) (h1 (h reduct))).
rewrite H102 mulmx0 mul0mx.
have ->: (0 + 0 + (0+0)= (addmx (addmx 0 0)(addmx 0 0))); first by done.
by rewrite !add0mx.
Qed.


Definition Reduction_red_red := Build_reduction_CC2 is_reduction_red_red.



End red_red_is_red_general.




Generated by coq2html