From Corelib Require Import Setoid.
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple.
From mathcomp Require Import finset tuple bigop.

Require Import tools.

Set Implicit Arguments.

Lemma enum_cast_ord m n (H : n = m):
  enum 'I_m = [seq cast_ord H i | i <- enum 'I_n].

Section Casts.

Lemma cast_map_cond (T: Type) n m (P : pred 'I_n) (F : 'I_n -> T) (H : m = n) :
  [seq F i | i <- enum 'I_n & P i] =
  [seq F (cast_ord H i) | i <- enum 'I_m & P (cast_ord H i) ].

Lemma mem_cast m n (H : m = n) (i : 'I_m) (S : {set 'I_m}) :
  (cast_ord H i) \in [set cast_ord H i | i in S] = (i \in S).

Definition cast_set n m (H : n = m) : {set 'I_n} -> {set 'I_m} :=
  [fun s : {set 'I_n} => (cast_ord H) @: s].

Lemma cast_set_inj n m (H : n = m) : injective (cast_set H).

Lemma cover_cast m n (P : {set {set 'I_n}}) (H : n = m) :
  cover (imset (cast_set H) (mem P)) = (cast_set H) (cover P).

End Casts.