proposition: Lemma weak_leq_gen_leq : forall (f:E1)(a x y:E), next_compatible f a -> inc y (U a) -> leq_gen f x y = leq a x y.
proof: Proof. ir. ap iff_eq; ir. uh H1. nin H1. ee. cp (next_compatible_or H H1). nin H3. apply linear_suborder_leq with x0. uh H; ee. uh H; ee; am. am. apply next_compatible_saturated with (f:=f)(a:= x0)(y:=y). am. am. am. am. am. am. apply is_suborder_leq with x0. am. am. uhg. sh a. ee. am. am. Qed.
imports: Arith order