proposition: Lemma inv_Sum2 : forall m n : nat, m <= S n -> forall f, [--] (Sum2 m n f) [=] Sum2 _ _ (fun i Hm Hn => [--] (f i Hm Hn)).
proof: Proof. intros m n H f. unfold Sum2 in |- *; simpl in |- *. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. 2: apply inv_Sum. apply Sum_wd; intro i. elim le_lt_dec; intro; simpl in |- *; elim le_lt_dec; intro; simpl in |- *; algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)