(* Constructions with pr_tl *************************************************)
(*** isdiv_tl *)
-lemma pr_isd_tl (f): ð\9d\9b\80â\9dªfâ\9d« â\86\92 ð\9d\9b\80â\9dªâ«°fâ\9d«.
+lemma pr_isd_tl (f): ð\9d\9b\80â\9d¨fâ\9d© â\86\92 ð\9d\9b\80â\9d¨â«°fâ\9d©.
#f cases (pr_map_split_tl f) * #H
[ elim (pr_isd_inv_push … H) -H //
| /2 width=3 by pr_isd_inv_next/