proposition: Lemma diamond_confluent : diamond R → confluent R.
proof: Proof. intros Hdiam. assert (∀ x y1 y2, rtc R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z) as Hstrip. { intros x y1 y2 Hy1; revert y2. induction Hy1 as [x|x y1 y1' Hy1 Hy1' IH]; [by eauto|]; intros y2 Hy2. destruct (Hdiam x y1 y2) as (z&Hy1z&Hy2z); auto. destruct (IH z) as (z'&?&?); eauto. } intros x y1 y2 Hy1; revert y2. induction Hy1 as [x|x y1 y1' Hy1 Hy1' IH]; [by eauto|]; intros y2 Hy2. destruct (Hstrip x y2 y1) as (z&?&?); eauto. destruct (IH z) as (z'&?&?); eauto using rtc_transitive. Qed.
imports: stdpp(options)