proposition: Lemma give_fin {m} (n : nat) {h : Lt n m} : ('fin m)%pack.
proof: Proof. cbn. exists n. exact h. Defined.
imports: Coq(Utf8 Lia) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) extructures(ord fset fmap) Crypt(Prelude Axioms ChoiceAsOrd RulesStateProb choice_type pkg_core_definition pkg_composition)