proposition: Lemma tot_ext_suc_irr A dom (r s: relation A) (SUC: Successor r s) (ACYC: acyclic r): irreflexive (tot_ext_suc dom r s).
proof: Proof. red in SUC; desc. unfold tot_ext_suc; ins. rewrite irreflexive_union; splits. by rewrite INC. rewrite irreflexive_seqC, !seqA, functional_path; [relsf | done]. rewrite irreflexive_union; splits. - rewrite seq_eqv_max_rt. generalize (tot_ext_irr dom ACYC); basic_solver. - rewrite irreflexive_seqC, !seqA. rewrite transp_seq_eqv_max_rt. generalize (tot_ext_irr dom ACYC); basic_solver. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn