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