proposition: Lemma tot_ext_nat_inv r x y : acyclic r -> tot_ext_nat r x y -> ~ r y x.
proof: Proof. red; ins; eapply tot_ext_nat_irr, tot_ext_nat_trans, tot_ext_nat_extends; eauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn