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