proposition: Lemma thinner_plus : forall x y z t, thinner x y -> thinner z t -> thinner (plus x z)(plus y t).
proof: Proof. intros [lx ux] [ly uy] [lz uz] [lt' ut] [H1 H2][H3 H4]; split; simpl. rewrite cp_min_comm; apply cp_min_plus; rewrite cp_min_comm; auto. rewrite cp_max_comm; apply cp_max_plus; rewrite cp_max_comm; auto. Qed.
imports: ZArith List Lia