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