proposition: Lemma subset_trans: subset s s'=true -> subset s' s''=true -> subset s s''=true.
proof: Proof. do 3 rewrite <- subset_iff; intros. apply subset_trans with s'; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx