fact: Fixpoint Sumx n : (forall i : nat, i < n -> G) -> G := match n return ((forall i : nat, i < n -> G) -> G) with | O => fun _ => [0]:G | S m => fun f => Sumx m (fun i l => f i (Nat.lt_lt_succ_r _ _ l)) [+]f m (Nat.lt_succ_diag_r m) end.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)