(* Properties with iterated next ********************************************)
lemma isdiv_nexts: ān,f. šāŖfā« ā šāŖā*[n]fā«.
-#n elim n -n /3 width=3 by isdiv_next/
+#n @(nat_ind_succ ā¦ n) -n /3 width=3 by isdiv_next/
qed.
(* Inversion lemmas with iterated next **************************************)
lemma isdiv_inv_nexts: ān,g. šāŖā*[n]gā« ā šāŖgā«.
-#n elim n -n /3 width=3 by isdiv_inv_next/
+#n @(nat_ind_succ ā¦ n) -n /3 width=3 by isdiv_inv_next/
qed.
(* Properties with tail *****************************************************)
(* Properties with iterated tail ********************************************)
lemma isdiv_tls: ān,g. šāŖgā« ā šāŖā«±*[n]gā«.
-#n elim n -n /3 width=1 by isdiv_tl/
+#n @(nat_ind_succ ā¦ n) -n /3 width=1 by isdiv_tl/
qed.