proposition: Lemma thinner_prop : forall i1 i2 x, thinner i1 i2 -> to_p i1 x -> to_p i2 x.
proof: Proof. intros [l1 u1][l2 u2] x [H1 H2] H3. destruct (to_p_cp_max_min _ _ _ H3). apply cp_max_min_to_p. rewrite cp_max_comm; apply cp_max_trans with l1. rewrite cp_max_comm; auto. apply cp_min_r_cp_max_l; auto. apply cp_min_trans with u1; auto. apply cp_max_r_cp_min_l; auto. Qed.
imports: ZArith List Lia