proposition: Lemma max_comp_scale_sym_sub: forall a b:E, sub (max_comp_scale a b) (max_comp_scale b a).
proof: Proof. ir. uhg; ir. ufi max_comp_scale H. cp (union_exists H). nin H0. ee. uf max_comp_scale; apply union_inc with x0. am. rwi compatibility_scales_inc H1. rw compatibility_scales_inc. uh H1; ee. uhg; xd. ir. sy. au. Qed.
imports: Arith order