proposition: Lemma N_le_succ_plus_1 : forall n m : N, (n + 1 <= m)%N <-> (n < m)%N.
proof: Proof. intros; rewrite N.add_1_r. apply N.le_succ_l. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program