proposition: Lemma fold_left_length : forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l.
proof: Proof. intros A l. induction l as [|? ? IH] using rev_ind; [reflexivity|]. now rewrite fold_left_app, app_length, IH, Nat.add_comm. Qed.
imports: PeanoNat