proposition: Lemma functional_inv_fsupp r (F: functional r⁻¹) : fsupp r.
proof: Proof. unfolder; ins. tertium_non_datur (exists x, r x y); ins; desf. - exists (x :: nil); ins; eauto. - exists nil; ins; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom