proposition: Lemma linear_not_lt_leq : forall a x y : E, is_linear a -> inc x (U a) -> inc y (U a) -> (lt a x y -> False) -> leq a y x.
proof: Proof. intros. unfold is_linear in H; ee. pose (H3 _ _ H0 H1). induction o. pose (leq_eq_or_lt H H4). induction o. rewrite H5. unfold axioms in H; ee. ap H; am. elim (H2 H5). am. Qed.
imports: universe