proposition: Lemma toNat_tcast: forall n m (bs: BITS n)(H: n = m), toNat (tcast H bs) = toNat bs.
proof: Proof. move=> n m bs H. by case: m / H. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations