proposition: Lemma clos_trans_immediate1 A (r : relation A) (T: transitive r) a b : (immediate r)⁺ a b -> r a b.
proof: Proof. unfold immediate; induction 1; desf; eauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath