proposition: Lemma N_lt_double: forall p : N, (0 < p)%N -> (p < 2 * p)%N.
proof: Proof. intros; replace (2 * p)%N with (p + p)%N by ring. replace p with (0 + p)%N at 1 by ring. rewrite <- N.add_lt_mono_r. assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program