proposition: Lemma mulC_rect x1 y1 x2 y2 : (x1 + 'i * y1) * (x2 + 'i * y2) = x1 * x2 - y1 * y2 + 'i * (x1 * y2 + x2 * y1).
proof: Proof. rewrite mulrDl !mulrDr (AC (2*2) (1*4*(2*3)))/= mulrACA. by rewrite -expr2 sqrCi mulN1r -!mulrA [_ * ('i * _)]mulrCA [_ * y1]mulrC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)