proposition: Lemma fsupp_ct_rt r : fsupp r⁺ -> fsupp r＊.
proof: Proof. rewrite rtE; eauto using fsupp_union, fsupp_eqv. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom