proposition: Lemma csumACA: interchange csum2 csum2.
proof: Proof. move => s1 s2 r1 r2; rewrite (csumA _ s2 r2) (csumA _ r1 r2). by rewrite -(csumA s1) (csumC s2 r1) (csumA s1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)