proposition: Lemma divC_Crect x1 y1 x2 y2 : (x1 + 'i * y1) / (x2 + 'i * y2) = (x1 * x2^* + y1 * y2^* + 'i * (x2^* * y1 - x1 * y2^*)) / `|x2 + 'i * y2| ^+ 2.
proof: Proof. rewrite invC_Crect// -mulrN [_ / _]rectC_mulr mulC_rect !mulrA -mulrBl. rewrite [_ * _ * y1]mulrAC -mulrDl mulrA -mulrDl !(mulrN, mulNr) opprK. by rewrite [- _ + _]addrC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)