proposition: Lemma tot_ext_suc_extends A dom (r s: relation A) (ACYC: acyclic r) (SUC: Successor r s) (IN: s ⊆ ⦗fun x => In x dom⦘ ⨾ s ⨾ ⦗fun x => In x dom⦘) : r ⊆ tot_ext_suc dom r s.
proof: Proof. arewrite (r ⊆ (r \ s⁺) ∪ s⁺). by apply inclusion_union_minus. arewrite (r \ s ⁺ ⊆ ⦗fun _ => True⦘ ⨾ (r \ s ⁺) ⨾ ⦗fun _ => True⦘). basic_solver. rewrite !last_exists_rewrite with (s:=s); [|cdes SUC; rewrite INC; done| edone]. rewrite !seqA. sin_rewrite succ_helper; [|by apply SUC]. rewrite inclusion_minus_rel. cdes SUC; rewrite INC at 3; rels. unfold tot_ext_suc. rewrite inclusion_t_ind with (r' := tot_ext dom r); [auto with hahn | red; eapply tot_ext_extends | apply tot_ext_trans]. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn