proposition: Lemma tot_ext_suc_trans A dom (r s: relation A) (SUC: Successor r s) : transitive (tot_ext_suc dom r s).
proof: Proof. unfold tot_ext_suc. apply transitiveI; relsf. repeat apply inclusion_union_l; eauto with hahn. - by rewrite ct_ct; rels. - rewrite inclusion_t_rt at 1. rewrite !seqA, functional_path; [relsf | apply SUC]. rewrite seq_eqv_max_rt. basic_solver 16. - rewrite !seqA. sin_rewrite functional_path; [relsf | apply SUC]. seq_rewrite seq_eqv_max_rt; relsf. seq_rewrite transp_seq_eqv_max_rt; relsf. arewrite_id (⦗max_elt s⦘) at 2; relsf. sin_rewrite rewrite_trans; [rels| apply tot_ext_trans]. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn