proposition: Lemma Cinv_mult_simpl : forall z1 z2 z3 : C, z1 <> C0 -> z1 * / z2 * (z3 * / z1) = z3 * / z2.
proof: Proof. intros z1 z2 z3 H. rewrite Cmult_assoc ; rewrite Cmult_comm ; rewrite Cmult_assoc. replace (z3 * /z1 * z1) with z3 by (field ; assumption). apply Cmult_comm. Qed.
imports: Ctacfield Cbase Cpow Lia