proposition: Lemma mulRACA x1 y1 x2 y2 : x1 * y1 * (x2 * y2) == x1 * x2 * (y1 * y2).
proof: Proof. by rewrite !mulRA (mulRAC x1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)