(*** isdiv_nexts *)
lemma gr_isd_nexts (n) (f): šāŖfā« ā šāŖā*[n]fā«.
#n @(nat_ind_succ ā¦ n) -n /3 width=3 by gr_isd_next/
qed.
(*** isdiv_nexts *)
lemma gr_isd_nexts (n) (f): šāŖfā« ā šāŖā*[n]fā«.
#n @(nat_ind_succ ā¦ n) -n /3 width=3 by gr_isd_next/
qed.