proposition: Lemma test_addr (R : comRingType) (a b c d : R) : (a + b + c + d = a + c + b + d)%R.
proof: Proof. time by rewrite -GRing.addrA GRing.addrAC GRing.addrA GRing.addrAC. Restart. Proof. time by rewrite (ACl (1*3*2*4)). Restart. Proof. time by rewrite (@GRing.add R).[ACl 1*3*2*4]. Qed.
imports: mathcomp(all_ssreflect ssralg)