proposition: Lemma Cmult_distributive_r : forall z1 z2 z3 : C, Cmult (Cplus z1 z2) z3 = Cplus (Cmult z1 z3) (Cmult z2 z3).
proof: Proof. intros. rewrite Cmult_commutative; rewrite Cmult_distributive. rewrite Cmult_commutative; rewrite (Cmult_commutative z3 z2); auto with geo. Qed.