proposition: Lemma fsupp_imm_t r (FS: fsupp r) (IRR: irreflexive r) (TRANS: transitive r) : r ≡ (immediate r)⁺.
proof: Proof. split; [|by eauto with hahn]. red; ins. specialize (FS y); desf. assert (M: forall n, r x n -> r n y -> In n findom) by eauto. clear FS; revert x y H M. induction findom using (well_founded_induction (well_founded_ltof _ (@length _))). unfold ltof in *. ins. tertium_non_datur (immediate r x y) as [|NIMM]; vauto. assert (N := M _ NIMM NIMM0); apply In_split in N; desf. apply t_trans with (y := n); eapply H with (y := l1 ++ l2); ins. 1,3: by rewrite !app_length; simpl; lia. - apply M in H1; eauto; rewrite !in_app_iff in *; ins; desf; eauto. exfalso; eauto. - apply M in H2; eauto; rewrite !in_app_iff in *; ins; desf; eauto. exfalso; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom