proposition: Lemma pow2_weakly_monotone : forall n m: nat, (n <= m) -> (pow2 n <= pow2 m).
proof: Proof. induction 1; simpl; try change (pow2 (S m)) with (2 * pow2 m); intuition. Qed.
imports: Coq.Program.Program Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeWrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Bedrock.Arrays Bedrock.Platform.Facade.examples.QsADTs Bedrock.Word