Require Export NatExt.
Require Export MatrixModule.

Include (MonoidMatrixTheory MonoidElementTypeNat).

Open Scope nat_scope.
Open Scope vec_scope.
Open Scope mat_scope.

Section test.

  Open Scope vec_scope.

  Let u := @l2v 3 [1;2;3].
  Let v := @f2v 3 (fun i => 5 + i)%nat.


  Open Scope mat_scope.

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

  Example mnth_ex1 : M.11 = 1.
  Proof. auto. Qed.

  Variable a11 a12 a21 a22 : A.
  Variable f : A -> A.
  Let M2 := @l2m 2 2 [[a11;a12];[a21;a22]].

End test.