proposition: Lemma linear_show_same : forall a b:E, (is_linear a) -> (is_linear b) -> (U a) = (U b) -> (forall (x y:E),(leq a x y) -> (leq b x y)) ->(same_order a b).
proof: Proof. ir. uhg; ee; ap show_is_suborder; ir. uh H; ee; am. uh H0; ee; am. ap H2; am. uh H0; ee; am. uh H; ee; am. uh H; ee. assert (inc x (U a)). rw H1. uh H0; ee. uh H0; ee. ap (H6 _ _ H3). assert (inc y (U a)). rw H1. uh H0; ee. uh H0; ee. ap (H8 _ _ H3). pose (H4 _ _ H5 H6). nin o. am. pose (H2 _ _ H7). uh H0; ee; uh H0; ee. assert (x = y). ap H11; am. rw H13. uh H; ee. ap H. am. Qed.
imports: Arith order