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