proposition: Lemma linear_suborder_leq : forall a b x y : E, is_linear a -> is_suborder a b -> inc x (U a) -> inc y (U a) -> leq b x y -> leq a x y.
proof: Proof. ir. ap linear_not_lt_leq. am. am. am. ir. assert (lt b y x). uhg; ee. apply is_suborder_leq with a. am. uh H4; ee; am. uh H4; ee; am. apply no_lt_leq with b y x. uh H0; ee. am. am. am. Qed.
imports: Arith order