proposition: Lemma Rintegral_domain_pow: forall c p r, ~c == 0 -> c * (pow p r) == ring0 -> p == ring0.
proof: Proof. intros. case (integral_domain_product c (pow p r) H0). - intros; absurd (c == ring0); auto. - intros. apply pow_not_zero with r. trivial. Qed.
imports: Cring