proposition: Lemma succ_helper A (r s: relation A) (SUC: s⁻¹ ⨾ r ⊆ r^?): s⁻¹＊ ⨾ (r \ s⁺) ⊆ r \ s⁺.
proof: Proof. eapply rt_ind_left with (P:= fun __ => __ ⨾ (r \ s⁺)); relsf. intros k IH. rewrite !seqA, IH; relsf. unfold seq, transp, minus_rel, clos_refl, inclusion in *. ins; desf; splits. assert (x = y \/ r x y) by eauto. by desf; destruct H1; vauto. by intro; apply H1; vauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn