proposition: Lemma wf_impl_no_inf_seq r (WF: well_founded r) x : ~ exists a, a 0 = x /\ forall n, r (a (S n)) (a n).
proof: Proof. specialize (WF x); induction WF. intro CONTRA; desf. specialize (CONTRA0 0) as C. apply H0 in C; destruct C. exists (fun n => a (S n)); ins. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom