(* Main inversions with pr_eq ***********************************************)
(*** isdiv_inv_eq_repl *)
(* Main inversions with pr_eq ***********************************************)
(*** isdiv_inv_eq_repl *)
#H cases (pr_eq_inv_next_sn … H) -H
/4 width=3 by pr_isd_next, pr_eq_trans/
qed.
(*** eq_next_inv_isdiv *)
#H cases (pr_eq_inv_next_sn … H) -H
/4 width=3 by pr_isd_next, pr_eq_trans/
qed.
(*** eq_next_inv_isdiv *)