proposition: Lemma cprod_An2 I J (f: fterm2): cprodb I (fun i => cprodb J (fun j => f i j)) = cprodb J (fun j => cprodb I (fun i => f i j)).
proof: Proof. exact: (proj2 (csum_prod_assoc_aux I J f)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)