proposition: Lemma cp_max_trans : forall x y z, cp_max x y = x -> cp_max y z = y -> cp_max x z = x.
proof: Proof. intros [x | | ] [y| |]; try (simpl; intros; discriminate); intros [z | | ]; try(simpl; intros; discriminate); simpl; auto. intros H1 H2; injection H1; injection H2; intros H3 H4. rewrite Zle_to_Zmax; auto. apply Z.le_trans with y. rewrite <- H3; apply Z.le_max_r. rewrite <-H4; apply Z.le_max_r. Qed.
imports: ZArith List Lia