#f #l #l1 #l2 #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) //
#Hi elim (nlt_ge_false l l)
/2 width=6 by pr_nat_inv_monotonic/
qed-.
theorem pr_nat_inj (f) (l1) (l2) (l):
#f #l #l1 #l2 #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) //
#Hi elim (nlt_ge_false l l)
/2 width=6 by pr_nat_inv_monotonic/
qed-.
theorem pr_nat_inj (f) (l1) (l2) (l):