#g * -g
#f #g #Hf * /2 width=3 by ex2_intro/
qed-.
(* Advanced inversion lemmas ************************************************)
#g * -g
#f #g #Hf * /2 width=3 by ex2_intro/
qed-.
(* Advanced inversion lemmas ************************************************)
#g #H elim (isdiv_inv_gen … H) -H
#f #Hf * -g #g #H elim (discr_push_next … H)
qed-.
(* Main inversion lemmas ****************************************************)
#g #H elim (isdiv_inv_gen … H) -H
#f #Hf * -g #g #H elim (discr_push_next … H)
qed-.
(* Main inversion lemmas ****************************************************)
#n elim n -n /3 width=3 by isdiv_next/
qed.
(* Inversion lemmas with iterated next **************************************)
#n elim n -n /3 width=3 by isdiv_next/
qed.
(* Inversion lemmas with iterated next **************************************)
#n elim n -n /3 width=3 by isdiv_inv_next/
qed.
(* Properties with tail *****************************************************)
#n elim n -n /3 width=3 by isdiv_inv_next/
qed.
(* Properties with tail *****************************************************)
#f cases (pn_split f) * #g * -f #H
[ elim (isdiv_inv_push … H) -H //
| /2 width=3 by isdiv_inv_next/
#f cases (pn_split f) * #g * -f #H
[ elim (isdiv_inv_push … H) -H //
| /2 width=3 by isdiv_inv_next/