proposition: Lemma Cmult_integral_contrapositive : forall z1 z2 : C, z1 <> C0 /\ z2 <> C0 -> z1 * z2 <> C0.
proof: Proof. intros z1 z2 H. destruct H as (H1, H2). intro H ; apply H1 ; apply Cmult_integral in H ; elim H ; intro Hdet. exact Hdet. rewrite Hdet in H2 ; destruct H2 ; reflexivity. Qed.
imports: Ctacfield Cbase Cpow Lia