proposition: Lemma Nmin_lt_4 a b c : Nleb (N.min b c) a = false -> Nleb c a = false.
proof: Proof. rewrite <- !not_true_iff_false, !Nleb_Nle. rewrite N.min_le_iff; auto. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits