proposition: Lemma cp_max_irreducible : forall a b, cp_max a b = a \/ cp_max a b = b.
proof: Proof. intros [a | | ][b | | ];try (intuition; fail). simpl; case (Zmax_irreducible_inf a b); intros H; rewrite H; auto. Qed.
imports: ZArith List Lia