fact: Definition norm_lists_ norm (l : nelist T) := fold_map' (fun u => return_prd (norm u)) (fun u l => add_to_prd (norm u) l) l.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)