proposition: Lemma length_firstn {A} : forall n (l: list A), n < List.length l -> List.length (firstn n l) = n.
proof: Proof. intros; rewrite firstn_length. apply Min.min_l; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega