proposition: Theorem digit_monotone : forall p q : Z, (Z.abs p <= Z.abs q)%Z -> digit p <= digit q.
proof: Proof. intros p q H; case (Nat.le_gt_cases (digit p) (digit q)); auto; intros H1; contradict H. apply Zlt_not_le. cut (p <> 0%Z); [ intros H2 | idtac ]. apply Z.lt_le_trans with (2 := digitLess p H2). cut (digit q <= pred (digit p)); [ intros H3 | idtac ]. apply Z.lt_le_trans with (2 := Zpower_nat_monotone_le _ _ H3); auto with zarith. apply digitMore. generalize H1; case (digit p); simpl in |- *; auto with arith. generalize H1; case p; simpl in |- *; intros tmp; intros; red in |- *; intros; try discriminate; contradict tmp; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz