proposition: Lemma tot_ext_suc_suc A dom (r s: relation A) (SUC: Successor r s) : Successor (tot_ext_suc dom r s) s.
proof: Proof. unfold Successor, tot_ext_suc in *; ins; desf; splits; auto with hahn. relsf. apply inclusion_union_l; ins. - rewrite ct_begin at 1. rewrite functional_alt in FUN; sin_rewrite FUN; basic_solver. - rewrite rt_begin at 1; relsf. apply inclusion_union_l; ins. * arewrite (s⁻¹ ⊆ (s⁻¹)＊) at 1. seq_rewrite transp_seq_eqv_max_rt; rels; basic_solver 20. * rewrite !seqA. rewrite functional_alt in FUN; sin_rewrite FUN; rels. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn