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