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