proposition: Lemma Nltb_double_mono a b : Nleb a b = false -> Nleb (N.double a) (N.double b) = false.
proof: Proof. intros. elim (sumbool_of_bool (Nleb (N.double a) (N.double b))). - intro H0. rewrite (Nleb_double_mono_conv _ _ H0) in H. discriminate H. - trivial. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits