proposition: Lemma Nltb_trans a b c : Nleb b a = false -> Nleb c b = false -> Nleb c a = false.
proof: Proof. unfold Nleb. intros. apply leb_correct_conv. apply Nat.lt_trans with (m := N.to_nat b). - apply leb_complete_conv. assumption. - apply leb_complete_conv. assumption. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits