I was trying one of the examples mentioned at the end of https://github.com/coq-community/coqeal/blob/1.1.3/refinements/seqmx.v#L1379C1-L1382C7

This one (with coqeal 1.1.3 and mathcomp-1):

```
From CoqEAL Require Import hrel param refinements trivial_seq.
From CoqEAL.refinements Require Import seqmx.
Goal ((0 : 'M[int]_(2,2)) == 0).
by coqeal.
Abort.
```

But that gave error (no applicable tactic).

The same `coqeal`

tactic without the `by`

leads to a loong term.

How can I make this work?

This went ahead though:

```
Goal ((0 : 'M[int]_(2,2)) == 0).
rewrite /const_mx //.
Qed.
```

Apparently there were a few missing require imports, the following works (the set of require import may not be minimal though):

```
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
From mathcomp Require Import ssralg matrix ssrint.
From CoqEAL Require Import hrel param refinements trivial_seq.
From CoqEAL Require Import binnat binint seqpoly binord seqmx.
Local Open Scope ring_scope.
Section testmx.
Goal ((0 : 'M[int]_(2,2)) == 0).
by coqeal.
Abort.
```

Last updated: Jul 15 2024 at 20:02 UTC