proposition: Lemma Nleb_double_plus_one_mono a b : Nleb a b = true -> Nleb (N.succ_double a) (N.succ_double b) = true.
proof: Proof. unfold Nleb. intros. rewrite !N2Nat.inj_succ_double. apply leb_correct. apply le_n_S, Nat.mul_le_mono_l. now apply leb_complete. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits