proposition: Lemma refine_format_nat : forall n ce, refine (format_nat n ce) (ret (encode_nat n ce)).
proof: Proof. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.ZArith.ZArith Bedrock.Word