proposition: Lemma max_comp_scale_bisubset : forall (a b :E), is_well_ordered a -> is_well_ordered b -> scale_bisubset a b (max_comp_scale a b).
proof: Proof. ir. uf max_comp_scale. ap scale_bisubset_union. am. am. ir. rwi compatibility_scales_inc H1. am. Qed.
imports: Arith order