proposition: Lemma addA x y z : x + (y + z) == x + y + z.
proof: Proof. wlog suffices: x y z / x + y + z <= x + (y + z). by split; rewrite // -!(addC z) !(addC x). move=> c [a ltxa [b ltyb ltzc]]; exists (a + b)%R; last by rewrite opprD addrA. by exists a; last rewrite addrC addKr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)