proposition: Lemma ad_S_le_then_neq : forall x y : ad, Nleb (ad_S x) y = true -> N.eqb x y = false.
proof: Proof. intros x y H. cut (N.eqb x y = true \/ N.eqb x y = false). intro H0. elim H0. clear H0. intro H0. cut (x = y). intro H1. rewrite H1 in H. unfold Nleb in H. rewrite (ad_S_is_S y) in H. cut (leb (S (nat_of_N y)) (nat_of_N y) = false). rewrite H. intro H2. discriminate H2. cut (nat_of_N y < S (nat_of_N y)). intro H2. apply leb_correct_conv. assumption. unfold lt in |- *. trivial. apply Neqb_complete. assumption. trivial. elim (N.eqb x y). auto. auto. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)