proposition: Lemma ad_S_le_then_le : forall x y : ad, Nleb (ad_S x) y = true -> Nleb x y = true.
proof: Proof. intros x y H. cut (Nleb x (ad_S x) = true). intro H0. apply Nleb_trans with (b := ad_S x). assumption. assumption. unfold Nleb in |- *. apply leb_correct. rewrite (ad_S_is_S x). apply le_S. apply le_n. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)