proposition: Lemma tot_ext_inv A dom r (x y : A) : acyclic r -> tot_ext dom r x y -> ~ r y x.
proof: Proof. red; ins; eapply tot_ext_irr, tot_ext_trans, tot_ext_extends; eauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn