小编ham*_*d k的帖子

我们知道 nat 的每个子集都有一个最小数。我能够证明这样的事情：

Variable P : nat -> Prop.
Hypothesis H : (exists n : nat , P n).

Theorem well_ordering : exists m : nat , P m /\ forall x : nat , x<m -> ~ P x.

但是我如何定义一个像 min_point 这样的函数？

Variable P : nat -> Prop.
Hypothesis H : (exists n : nat , P n).

Definition min_point : nat.

Theorem min_point_def : P min_point /\ forall x : nat , x<min_point -> ~ P x. 

例如我有这个样本记录：

Record Sample := {
  SA :> nat ; 
  SB :> Z ; 
  SCond : Z.abs_nat SB <> SA
}.

当我想证明这个引理时：

Lemma Sample_eq : forall a b : Sample , a = b <-> SA a = SA b /\ SB a = SB b.

我看到这个：

1 subgoal
______________________________________(1/1)
forall a b : Sample, a = b <-> a = b /\ a = b

问题 1：如何强制 Coq 显示 SA a 而不是 a？

问题 2：如何证明这个引理？