proposition: Theorem well_founded_ltof : well_founded A ltof.
proof: Proof. red in |- *. cut (forall (n : nat) (a : A), f a < n -> Acc ltof a). intros H a; apply (H (S (f a))); auto with arith. induction n. intros; absurd (f a < 0); auto with arith. intros a ltSma. apply Acc_intro. unfold ltof in |- *; intros b ltfafb. apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid