proposition: Theorem Z2Nat_sub_min : ∀ x y, Z.to_nat (x - Z.min x y) = Z.to_nat (x - y).
proof: Proof. intros x y. destruct (Z.min_dec x y) as [H₁| H₁]. rewrite H₁. rewrite Z.sub_diag. apply Z.min_l_iff in H₁. apply Z.le_sub_0 in H₁. destruct (x - y)%Z as [| p| p]; [ reflexivity | idtac | reflexivity ]. apply Z.nlt_ge in H₁. exfalso; apply H₁, Pos2Z.is_pos. rewrite H₁; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz