proposition: Lemma inv_Sumx : forall n f, [--] (Sumx n f) [=] Sumx _ (fun i Hi => [--] (f i Hi)).
proof: Proof. intro n; induction n as [| n Hrecn]. simpl in |- *; algebra. intro f; simpl in |- *. astepl ([--] (Sumx _ (fun i (l : i < n) => f i (Nat.lt_lt_succ_r i n l))) [+] [--] (f n (Nat.lt_succ_diag_r n))). apply bin_op_wd_unfolded. apply Hrecn with (f := fun i (l : i < n) => f i (Nat.lt_lt_succ_r i n l)). algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)