def internal_nat_foldl_op_eq_foldr_op_sym

bend-mathlib@0.8.1.0 · algebra.bend:504

import Base

504# Calls of the twins, as the calls above the generated section make of their laws (PLAN F38).
505def internal_nat_foldl_op_eq_foldr_op_sym(+xs: List<&2, Nat>) -> {List.foldr(&2, Nat, Nat, Nat.add, xs, 0n) == List.foldl(&2, Nat, Nat, Nat.add, xs, 0n) : Nat}:
506  foldl_op_eq_foldr_op_sym(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, ~0n, ~internal_nat_zero_add, xs)