proposition: Lemma N_lt_double_lt: forall p p' : N, (p < p')%N -> (2 * p < 2 * p')%N.
proof: Proof. intros; apply N.mul_lt_mono_pos_l; eauto; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program