proposition: Lemma next_compatible_saturated : forall (f:E1)(a b x y:E), next_compatible f a -> next_compatible f b -> inc y (U b) -> leq a x y -> inc x (U b).
proof: Proof. ir. nin (next_compatible_or H H0). uh H3; ee. ap H5. uh H2; ee; am. uh H3; ee. util (next_comp_sub_scale (f:= f) (a:=b) (b:=a)). am. am. am. uh H7; ee. apply H9 with y. am. am. Qed.
imports: Arith order