Ssreflect Users Discussion List

[Reynald Affeldt <>]

Hello,

I am afraid it is an easy question that just reveals my lack
of understanding.
How am I supposed to prove the following facts?

    Reynald

--

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype finfun 
finset prime.
Require Import groups zmodp ssralg perm matrix bigops.

Open Local Scope ring_scope.

Lemma coucou : forall (F : fieldType) n (s : 'S_n) (z : matrix F 1 n) j,
  Matrix [ffun ij => z ij.1 (s ij.2)] 0 j = z 0 (s j).
Proof.
Abort.

Lemma beuh : forall (F : fieldType) n (s : 'S_n) (z : matrix F 1 n) i j,
  (\matrix_(i0, j0) (if s i0 == j0 then 1 else 0)) i j = if s i == j then 
(GRing.one F) else (GRing.one F).
Proof.
Abort.