proposition: Lemma thinner_join_left : forall i i', thinner i (join i i').
proof: Proof. intros [b1 u1] [b2 u2]; split. destruct b1 as [l | | ]; destruct b2 as [l' | | ]; simpl; auto. rewrite Z.min_assoc; rewrite Zmin_idempotent; auto. rewrite Zmin_idempotent; auto. destruct u1 as [l | | ]; destruct u2 as [l' | | ]; simpl; auto. rewrite Z.max_assoc; rewrite Zmax_idempotent; auto. rewrite Zmax_idempotent; auto. Qed.
imports: ZArith List Lia