fact: Fixpoint count from n := match n with | O => nil | S x => from :: (count (from + 1) x) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing