proposition: Lemma foldl_foldr x0 l : foldl f x0 l = foldr f x0 l.
proof: Proof. elim: l x0 => [//|x1 l IHl] x0 /=; rewrite {}IHl. by elim: l x0 x1 => [//|x2 l IHl] x0 x1 /=; rewrite IHl !fA [f x2 x1]fC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)