fact: Fixpoint cumul (n : nat) (l : list N) {struct n} : list N := match n with | 0%nat => nil | 1%nat => hd 0 l :: nil | S (S _ as n1) => let a := hd 0 l in let l1 := tl l in let b := hd 0 l1 in if a =? b then (a + b) :: cumul n1 (tl l1) else a :: cumul n1 l1 end.
imports: Ascii String List EqNat NArith