Require Export Complex.
Require Export MatrixModule.

Include (FieldMatrixTheory FieldElementTypeC).

Open Scope C_scope.
Open Scope vec_scope.
Open Scope mat_scope.

Section test.

  Open Scope vec_scope.

  Let u := @l2v 3 [1 +i 2; 3 +i 4; 5 +i 6].
  Let v := @l2v 3 [0 +i 2; 3 +i 4; 5 +i 6].


  Open Scope mat_scope.

  Let M := @l2m 2 2 [[1 +i 2; 3 +i 4];[5 +i 6; 7 +i 8]].

  Example mat_C_ex1 : forall r c s (m1 m2 : mat r c) (m3 : mat c s),
      (m1 - m2) * m3 = m1 * m3 - m2 * m3.
  Proof.
    intros. rewrite mmul_msub_distr_r. auto.
  Qed.

  Example mat_C_ex2 : forall r c (m1 m2 : mat r c) x, m1 = m2 -> x c* m1 = x c* m2.
  Proof. intros. f_equal. auto. Qed.

  Example mat_C_ex3 : forall r c (m1 m2 : mat r c),
      (mat0 + m1) - (mat0 - m2) = m2 + (m1 - mat0).
  Proof.
    intros.
    pose proof (madd_AGroup r c). agroup.
  Qed.

End test.