proposition: Theorem fsupp_well_founded r (FS: fsupp r) (IRR: irreflexive r) (TRANS: transitive r) : well_founded r.
proof: Proof. intros a; specialize (FS a); desf; revert a FS. induction findom using (well_founded_induction (well_founded_ltof _ (@length _))). unfold ltof in *. constructor; intros y Rya. assert (IN := FS _ Rya). apply In_split in IN; desf. eapply (H (l1 ++ l2)); ins. by rewrite !app_length; simpl; lia. assert (Rxa: r x a) by eauto. generalize (FS _ Rxa); rewrite !in_app_iff; ins; desf; eauto. exfalso; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom