proposition: Lemma Nltb_leb_weak a b : Nleb b a = false -> Nleb a b = true.
proof: Proof. unfold Nleb. intros. apply leb_correct. apply Nat.lt_le_incl. apply leb_complete_conv. assumption. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits