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