proposition: Lemma next_compatible_same : forall (f:E1) (a b : E), next_compatible f a -> next_compatible f b -> U a = U b -> same_order a b.
proof: Proof. ir. cp (next_compatible_or H H0). nin H2. ap linear_show_same. uh H; ee. uh H; ee. am. uh H0; ee; uh H0; ee; am. am. ir. apply is_suborder_leq with a. am. am. ap linear_show_same. uh H; ee. uh H; ee. am. uh H0; ee; uh H0; ee; am. am. ir. ap linear_not_lt_leq. uh H0; ee; uh H0; ee; am. wr H1. uh H3; xd. wr H1; uh H3; xd. ir. assert (lt a y x). uhg; ee. uh H4; ee. apply is_suborder_leq with b; am. uh H4; ee; am. apply no_lt_leq with a y x. uh H; ee; uh H; ee; uh H; ee; am. am. am. Qed.
imports: Arith order