proposition: Lemma Nleb_double_mono_conv a b : Nleb (N.double a) (N.double b) = true -> Nleb a b = true.
proof: Proof. unfold Nleb. rewrite !N2Nat.inj_double. intro. apply leb_correct. apply <- (Nat.mul_le_mono_pos_l (N.to_nat a) (N.to_nat b) 2); auto. now apply leb_complete. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits