proposition: Theorem digitNotZero : forall q : Z, q <> 0%Z -> 0 < digit q.
proof: Proof. intros q H'. apply Nat.lt_le_trans with (m := digit 1); auto with zarith. apply digit_monotone. generalize H'; case q; simpl in |- *; auto with zarith; intros q'; case q'; simpl in |- *; auto with zarith arith; intros; red in |- *; simpl in |- *; red in |- *; intros; discriminate. Qed.
imports: Reals ZArith List PeanoNat Psatz