proposition: Lemma minus_pred_nat : forall (n m : Z) (Hn : (0 < n)%Z) (Hm : (0 < m)%Z) (Hnm : (0 < n - m)%Z), S (pred_nat n Hn) - S (pred_nat m Hm) = S (pred_nat (n - m) Hnm).
proof: Proof. intros. simpl in |- *. destruct n; try discriminate Hn. destruct m; try discriminate Hm. unfold pred_nat at 1 2 in |- *. rewrite minus_pred; try apply lt_O_nat_of_P. apply eq_inj. rewrite <- pred_nat_unfolded. rewrite Znat.inj_minus1. repeat rewrite ZL9. reflexivity. apply le_inj. apply Zlt_le_weak. repeat rewrite ZL9. apply Zlt_O_minus_lt. assumption. Qed.
imports: Coq(Lia)