proposition: Lemma compatibility_scales_inc : forall a b y : E, inc y (compatibility_scales a b) = scale_bisubset a b y.
proof: Proof. ir. ap iff_eq; ir. ufi compatibility_scales H; Ztac. uf compatibility_scales; ap Z_inc. ap powerset_inc. uh H; ee. uh H1; ee. am. am. Qed.
imports: Arith order