proposition: Lemma skip_S_length {A} : forall (l l': list A) a, l' = (skipn (S (length l)) (l ++ a :: l')).
proof: Proof. intros; rewrite <- app_cons_app_app_cons, ListFacts.rw_skipn_app. - reflexivity. - rewrite app_length; simpl; try omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.CertifiedExtraction.Extraction.Extraction Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Wrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Coq.Program.Program Coq.Lists.List Bedrock.Platform.Facade.examples.QsADTs