fact: Fixpoint tot_ext A (dom : list A) (r : relation A) : relation A := match dom with | nil => r⁺ | x::l => one_ext x (tot_ext l r) end.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn