proposition: Lemma clos_trans_immediate2 A (r : relation A) (T: transitive r) (IRR: irreflexive r) dom (D: domb r (fun x => In x dom)) a b : r a b -> (immediate r)⁺ a b.
proof: Proof. assert (D': forall c, r a c -> r c b -> In c dom). by ins; apply D in H; desf. clear D; revert a b D'. remember (length dom) as n; revert dom Heqn; induction n. by destruct dom; ins; vauto. ins; destruct (classic (exists c, r a c /\ r c b)); desf. 2: by eapply t_step; split; ins; eauto. forward eapply D' as X; eauto; apply in_split in X; desf. rewrite app_length in *; ins; rewrite <- plus_n_Sm, <- app_length in *; desf. apply t_trans with c; eapply IHn with (dom := l1 ++ l2); ins; forward eapply (D' c0); eauto; rewrite !in_app_iff; ins; desf; eauto; exfalso; eauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath