proposition: Theorem Z2Nat_sub_min2 : ∀ x y z, (Z.to_nat (Z.min x y - z) + Z.to_nat (x - y))%nat = Z.to_nat (x - Z.min y z).
proof: Proof. intros x y z. rewrite <- Z.sub_min_distr_r. rewrite <- Z.sub_max_distr_l. destruct (Z_le_dec (x - z) (y - z)) as [Hle₁| Hgt₁]. rewrite Z.min_l; [ idtac | assumption ]. apply Z.sub_le_mono_r in Hle₁. destruct (Z_le_dec (x - y) (x - z)) as [Hle₂| Hgt₂]. rewrite Z.max_r; [ idtac | assumption ]. rewrite Z.sub_le_mono_r with (p := y) in Hle₁. rewrite Z.sub_diag in Hle₁. rewrite Nat.add_comm. destruct (x - y)%Z as [| p| p]; [ reflexivity | idtac | reflexivity ]. apply Z.le_ngt in Hle₁. exfalso; apply Hle₁, Pos2Z.is_pos. apply Z.nle_gt, Z.lt_le_incl in Hgt₂. rewrite Z.max_l; [ idtac | assumption ]. apply Z.sub_le_mono_l in Hgt₂. eapply Z.le_trans in Hgt₂; [ idtac | eassumption ]. rewrite Z.sub_le_mono_r with (p := z) in Hgt₂. rewrite Z.sub_diag in Hgt₂. destruct (x - z)%Z as [| p| p]; [ reflexivity | idtac | reflexivity ]. apply Z.le_ngt in Hgt₂. exfalso; apply Hgt₂, Pos2Z.is_pos. apply Z.nle_gt, Z.lt_le_incl in Hgt₁. rewrite Z.min_r; [ idtac | assumption ]. apply Z.sub_le_mono_r in Hgt₁. destruct (Z_le_dec (x - y) (x - z)) as [Hle₂| Hgt₂]. rewrite Z.max_r; [ idtac | assumption ]. apply Z.sub_le_mono_l in Hle₂. rewrite Z.sub_le_mono_r with (p := y) in Hgt₁. rewrite Z.sub_diag in Hgt₁. rewrite Z.sub_le_mono_r with (p := z) in Hle₂. rewrite Z.sub_diag in Hle₂. rewrite <- Z2Nat.inj_add; [ idtac | assumption | assumption ]. rewrite Z.add_comm, Z.add_sub_assoc, Z.sub_add. reflexivity. apply Z.nle_gt, Z.lt_le_incl in Hgt₂. rewrite Z.max_l; [ idtac | assumption ]. apply Z.sub_le_mono_l in Hgt₂. rewrite Z.sub_le_mono_r with (p := z) in Hgt₂. rewrite Z.sub_diag in Hgt₂. destruct (y - z)%Z as [| p| p]; [ reflexivity | idtac | reflexivity ]. apply Z.le_ngt in Hgt₂. exfalso; apply Hgt₂, Pos2Z.is_pos. Qed.
imports: Utf8 QArith NPeano Sorted Psatz