proposition: Lemma Cmult_eq_0_compat : forall z1 z2 : C, z1 = C0 \/ z2 = C0 -> z1 * z2 = C0.
proof: Proof. intros z1 z2 H; elim H ; intros H1. rewrite H1 ; rewrite Cmult_0_l ; reflexivity. rewrite H1 ; rewrite Cmult_0_r ; reflexivity. Qed.
imports: Ctacfield Cbase Cpow Lia