proposition: Lemma cp_min_plus : forall x y z t, cp_min x y = x -> cp_min z t = z -> cp_min (comp_add x z)(comp_add y t)= comp_add x z.
proof: Proof. intros [x | | ] [y | | ];simpl;try (intros;discriminate); intros [z | | ] [t' | | ];simpl; try (intros; discriminate); auto. intros H1 H2; injection H1; injection H2; intros H4 H3. apply f_equal with (f:=cZ); apply Zle_to_Zmin. apply Z.le_trans with (x + t'). apply Zplus_le_compat_l; rewrite <- H4; apply Z.le_min_r. apply Zplus_le_compat_r; rewrite <- H3; apply Z.le_min_r. Qed.
imports: ZArith List Lia