proposition: Lemma next_compatible_or : forall (f : E1) (a b : E), next_compatible f a -> next_compatible f b -> (is_suborder a b \/ is_suborder b a).
proof: Proof. ir. cp (max_comp_scale_or H H0). nin H1. ap or_introl. ap full_bisubset_suborder. wr H1. ap max_comp_scale_bisubset. uh H; ee; am. uh H0; ee; am. ap or_intror. ap full_bisubset_suborder. rwi max_comp_scale_sym H1. wr H1. ap max_comp_scale_bisubset. uh H0; ee; am. uh H; ee; am. Qed.
imports: Arith order