proposition: Lemma immediate_clos_trans_elim A (r : relation A) a b : immediate r⁺ a b -> r a b /\ (forall c, r⁺ a c -> r⁺ c b -> False).
proof: Proof. unfold immediate; ins; desf; split; ins. apply t_step_rt in H; desf. apply clos_refl_transE in H1; desf; exfalso; eauto using t_step. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath