proposition: Lemma max_comp_scale_or : forall (f:E1) (a b : E), next_compatible f a -> next_compatible f b -> (max_comp_scale a b = U a) \/ (max_comp_scale a b = U b).
proof: Proof. ir. ap excluded_middle. uhg; ir. assert (~(max_comp_scale a b = U a)). ap excluded_middle; uhg; ir. ap H1; ap or_introl. ap excluded_middle; am. assert (~(max_comp_scale a b = U b)). ap excluded_middle; uhg; ir. ap H1; ap or_intror. ap excluded_middle; am. set (y:= max_comp_scale a b). assert (scale_bisubset a b y). uf y. ap max_comp_scale_bisubset. uh H; ee. am. uh H0; ee; am. assert (strict_sub y (U a)). uhg; ee. am. uh H4; ee. uh H6; ee; am. assert (strict_sub y (U b)). uhg; ee. am. uh H4; ee. uh H8; ee; am. assert (scale_bisubset a b (tack_on y (f y))). ap scale_bicompatible_next; au. wri compatibility_scales_inc H7. assert (sub (tack_on y (f y)) y). uhg; ir. uf y. uf max_comp_scale. apply union_inc with (tack_on y (f y)). am. am. assert (inc (f y) y). ap H8. rw tack_on_inc. ap or_intror; tv. assert (next a y = f y). ap next_compatible_scale. am. uh H4; ee; am. am. apply next_not_inc with a y. am. uh H; ee; am. rw H10; am. Qed.
imports: Arith order