proposition: Lemma confluent_alt : confluent R ↔ (∀ x y, rtsc R x y → ∃ z, rtc R x z ∧ rtc R y z).
proof: Proof. split. - intros Hcr. induction 1 as [x|x y1 y1' [Hy1|Hy1] Hy1' (z&IH1&IH2)]; eauto. destruct (Hcr y1 x z) as (z'&?&?); eauto using rtc_transitive. - intros Hcr x y1 y2 Hy1 Hy2. apply Hcr; trans x; eauto using rtc_rtsc_rl, rtc_rtsc_lr. Qed.
imports: stdpp(options)