proposition: Theorem digit_anti_monotone_lt : (1 < n)%Z -> forall p q : Z, digit p < digit q -> (Z.abs p < Z.abs q)%Z.
proof: Proof. intros H' p q H'0. case (Zle_or_lt (Z.abs q) (Z.abs p)); auto; intros H'1. contradict H'0. case (Zle_lt_or_eq _ _ H'1); intros H'2. apply Nat.le_ngt; auto with arith. now apply digit_monotone. rewrite <- (digit_abs p); rewrite <- (digit_abs q); rewrite H'2; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz