proposition: Lemma divC_rect x1 y1 x2 y2 : x1 \is real -> y1 \is real -> x2 \is real -> y2 \is real -> (x1 + 'i * y1) / (x2 + 'i * y2) = (x1 * x2 + y1 * y2 + 'i * (x2 * y1 - x1 * y2)) / (x2 ^+ 2 + y2 ^+ 2).
proof: Proof. by move=> *; rewrite divC_Crect normC2_rect ?conj_Creal. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)