proposition: Lemma foldl_rcons {T T0 : Type} : forall (f : T -> T0 -> T) x0 s t, foldl f x0 (rcons s t) = f (foldl f x0 s) t.
proof: Proof. move => f x0 s ; elim: s x0 => //= t s IH x0 t0 ; by rewrite IH. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)