Require Import mathcomp.ssreflect.ssreflect.
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].

Lemma nth_ord_ltn i n (H : i < n) x0 : nth x0 (enum 'I_n) i = (Ordinal H).

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.