isabelle/valid/induction_divisibility_9div10tonm1.thy (12 lines of code) (raw):
(*
Authors: Wenda Li
*)
theory induction_divisibility_9div10tonm1
imports
Complex_Main
begin
theorem induction_divisibility_9div10tonm1:
fixes n::nat
shows "(9::nat) dvd 10^n - 1"
sorry
end