proposition: Lemma test_addn (a b c d : nat) : a + b + c + d = a + c + b + d.
proof: Proof. time by rewrite -addnA addnAC addnA addnAC. Restart. Proof. time by rewrite (ACl (1*3*2*4)). Restart. Proof. time by rewrite addn.[ACl 1*3*2*4]. Qed.
imports: mathcomp(all_ssreflect ssralg)