/2 width=4 by pr_pat_mono/ qed-.
(* Main constructions with pr_id ********************************************)
(*** at_div_id_dx *)
theorem pr_pat_div_id_dx (f):
/2 width=4 by pr_pat_mono/ qed-.
(* Main constructions with pr_id ********************************************)
(*** at_div_id_dx *)
theorem pr_pat_div_id_dx (f):